| 6561b69 | Pierre-Yves Strub | 19 November 2021, 22:43:31 UTC | prune virtual tc | 19 November 2021, 22:43:31 UTC |
| 6b929c7 | Pierre-Yves Strub | 19 November 2021, 22:36:16 UTC | fix op types in typeclasses instances | 19 November 2021, 22:36:16 UTC |
| 1b3a699 | Pierre-Yves Strub | 19 November 2021, 15:51:21 UTC | Merge branch '1.0' into deploy-tc | 19 November 2021, 15:51:21 UTC |
| 54bb1fc | Pierre-Yves Strub | 19 November 2021, 15:50:50 UTC | WIP | 19 November 2021, 15:50:50 UTC |
| 1d6dc3d | Antoine Séré | 19 November 2021, 11:03:34 UTC | Bugs found | 19 November 2021, 11:03:34 UTC |
| 3476312 | Pierre-Yves Strub | 19 November 2021, 10:53:40 UTC | script for graphing a dependency graph for .eco | 19 November 2021, 10:53:40 UTC |
| 08ed0c2 | Pierre-Yves Strub | 19 November 2021, 07:18:43 UTC | New format for eco (v3) Store whether a theory has been directly required or not. | 19 November 2021, 07:18:46 UTC |
| 471ea3b | Pierre-Yves Strub | 19 November 2021, 07:03:57 UTC | foo | 19 November 2021, 07:04:08 UTC |
| a549eb4 | Pierre-Yves Strub | 19 November 2021, 06:23:34 UTC | Add an option to define opaque operators This can be done by adding the "opaque" tag, e.g.: op [opaque] myop = ... solve #94 | 19 November 2021, 06:27:09 UTC |
| 10e1563 | Pierre-Yves Strub | 19 November 2021, 06:09:01 UTC | remove \# files | 19 November 2021, 06:09:01 UTC |
| ffe0656 | Pierre-Yves Strub | 18 November 2021, 14:23:49 UTC | New command: locate [partial-qualid] This command allows to locate and print the fullname & shortest name of an operator, a lemma or a type declaration. fix #82 | 18 November 2021, 14:23:49 UTC |
| 92f23db | Pierre-Yves Strub | 18 November 2021, 12:06:18 UTC | Add the project name in dune-project This is needed by "dune subst" ref #99 | 18 November 2021, 12:06:45 UTC |
| 5e3929a | Pierre-Yves Strub | 18 November 2021, 12:06:09 UTC | remove debugging code | 18 November 2021, 12:06:09 UTC |
| dd3f68e | Antoine Séré | 17 November 2021, 19:11:57 UTC | Cleaned up examples/typeclass.ec | 17 November 2021, 19:11:57 UTC |
| 17e143c | Pierre-Yves Strub | 17 November 2021, 15:41:35 UTC | | 17 November 2021, 15:41:35 UTC |
| b38a5aa | Pierre-Yves Strub | 17 November 2021, 15:39:37 UTC | | 17 November 2021, 15:39:37 UTC |
| dfb413d | Pierre-Yves Strub | 17 November 2021, 15:35:07 UTC | fix opam package (do not do "dune subst") | 17 November 2021, 15:35:07 UTC |
| 619941e | Pierre-Yves Strub | 17 November 2021, 09:10:57 UTC | Merge branch '1.0' into deploy-tc | 17 November 2021, 09:10:57 UTC |
| 0a2d4ad | Pierre-Yves Strub | 17 November 2021, 07:42:42 UTC | [build] use dune to install & find resources | 17 November 2021, 08:23:14 UTC |
| 31ce231 | François Dupressoir | 06 November 2019, 20:46:14 UTC | [SmtMap] add has, find and some lemmas these are focused on a specific proof and deserve expanding, fleshing out and cleaning up | 17 November 2021, 07:51:50 UTC |
| 229ac7a | Pierre-Yves Strub | 17 November 2021, 06:24:47 UTC | Remove EcFortune | 17 November 2021, 06:24:47 UTC |
| 02082bd | Pierre-Yves Strub | 17 November 2021, 06:22:22 UTC | Update copyright | 17 November 2021, 06:22:22 UTC |
| e7d401f | Pierre-Yves Strub | 17 November 2021, 05:59:48 UTC | remove the script for creating tarballs | 17 November 2021, 06:01:10 UTC |
| e46ef74 | Pierre-Yves Strub | 17 November 2021, 05:57:03 UTC | disable warning as errors | 17 November 2021, 05:57:03 UTC |
| a54cec2 | Pierre-Yves Strub | 17 November 2021, 05:52:23 UTC | remove deprecated functions and reenable warning 3 | 17 November 2021, 05:52:23 UTC |
| b7a2ee2 | Pierre-Yves Strub | 17 November 2021, 05:43:59 UTC | reenable warning 39 | 17 November 2021, 05:43:59 UTC |
| 4217836 | Pierre-Yves Strub | 17 November 2021, 05:41:36 UTC | reenable warning 38 | 17 November 2021, 05:41:36 UTC |
| 061e164 | Pierre-Yves Strub | 17 November 2021, 05:40:28 UTC | reenable warning 35 | 17 November 2021, 05:40:28 UTC |
| 43a1b9f | Pierre-Yves Strub | 17 November 2021, 05:39:00 UTC | reenable warning 34 | 17 November 2021, 05:39:17 UTC |
| 5b09921 | Pierre-Yves Strub | 17 November 2021, 05:34:48 UTC | reenable warning 6 | 17 November 2021, 05:34:48 UTC |
| 003fc41 | Pierre-Yves Strub | 17 November 2021, 05:34:23 UTC | [build] only consider src/theories/examples are deps | 17 November 2021, 05:34:23 UTC |
| df78b65 | Pierre-Yves Strub | 17 November 2021, 05:34:13 UTC | .gitignore (.eca at root) | 17 November 2021, 05:34:13 UTC |
| f8d5b79 | Pierre-Yves Strub | 16 November 2021, 18:32:37 UTC | Merge pull request #31 from ejgallego/1.0+dune [build] Add basic dune support | 16 November 2021, 18:32:37 UTC |
| e39463d | Pierre-Yves Strub | 16 November 2021, 17:37:59 UTC | .gitignore: cleanup | 16 November 2021, 17:37:59 UTC |
| 68bbd4b | Pierre-Yves Strub | 16 November 2021, 14:59:38 UTC | [nix] update dependencies | 16 November 2021, 17:35:05 UTC |
| f7c671c | Pierre-Yves Strub | 16 November 2021, 14:14:36 UTC | [build] use dune in Makefile | 16 November 2021, 17:35:05 UTC |
| 5334126 | Pierre-Yves Strub | 16 November 2021, 13:38:29 UTC | [build] do not create an internal EC library we do not currently expose any stable API. | 16 November 2021, 17:35:05 UTC |
| 3f13dec | Pierre-Yves Strub | 16 November 2021, 13:29:42 UTC | Use the old build system in opam. | 16 November 2021, 17:35:04 UTC |
| fd804d6 | Emilio Jesus Gallego Arias | 22 August 2019, 15:33:19 UTC | [build] Add basic dune support Add experimental support for buidling `ec` using dune. Use ``` dune build ``` We don't add support for building the stdlib yet. | 16 November 2021, 17:35:04 UTC |
| 743a247 | Pierre-Yves Strub | 16 November 2021, 16:53:15 UTC | [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t | 16 November 2021, 17:35:04 UTC |
| 4b604bf | Christian Doczkal | 04 November 2021, 14:52:23 UTC | renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE | 16 November 2021, 17:35:04 UTC |
| ab62416 | Christian Doczkal | 24 October 2021, 10:45:16 UTC | adapt to consistent use of mu1 | 16 November 2021, 17:35:04 UTC |
| 15946aa | Christian Doczkal | 24 October 2021, 09:36:02 UTC | use mu1 instead of mass in in Distr | 16 November 2021, 17:35:04 UTC |
| 5a0238b | Pierre-Yves Strub | 16 November 2021, 16:53:15 UTC | [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t | 16 November 2021, 16:56:20 UTC |
| 8fd25e4 | Pierre-Yves Strub | 16 November 2021, 16:23:33 UTC | | 16 November 2021, 16:23:33 UTC |
| 2ce431b | Pierre-Yves Strub | 16 November 2021, 16:22:01 UTC | better formatting of error msgs | 16 November 2021, 16:22:01 UTC |
| 674e283 | Pierre-Yves Strub | 16 November 2021, 16:13:42 UTC | TC: fix parsing | 16 November 2021, 16:13:42 UTC |
| b4f19d5 | Pierre-Yves Strub | 16 November 2021, 15:58:30 UTC | better error messages for TC | 16 November 2021, 15:58:30 UTC |
| 9c8e467 | Pierre-Yves Strub | 16 November 2021, 15:40:47 UTC | fix instanciation op/axioms in tc instances | 16 November 2021, 15:40:47 UTC |
| c13bc35 | Pierre-Yves Strub | 16 November 2021, 15:28:41 UTC | fix type classes resolution for type variables | 16 November 2021, 15:28:41 UTC |
| d68d4cc | Pierre-Yves Strub | 16 November 2021, 15:15:58 UTC | fix merge (section / typeclass) | 16 November 2021, 15:15:58 UTC |
| 0a1eead | Antoine Séré | 16 November 2021, 13:42:21 UTC | Merge branch 'deploy-tc' of github:EasyCrypt/easycrypt into deploy-tc | 16 November 2021, 13:42:21 UTC |
| 6a7f430 | Antoine Séré | 16 November 2021, 13:42:01 UTC | added inherited instances | 16 November 2021, 13:42:01 UTC |
| d075d95 | Pierre-Yves Strub | 16 November 2021, 07:56:07 UTC | Merge branch '1.0' into deploy-tc | 16 November 2021, 07:56:07 UTC |
| cc70db8 | Pierre-Yves Strub | 15 November 2021, 14:21:23 UTC | type class inference | 15 November 2021, 14:21:23 UTC |
| 9303f9a | Pierre-Yves Strub | 15 November 2021, 12:45:24 UTC | generalize unification API for external constraints | 15 November 2021, 12:45:24 UTC |
| ec1f979 | Pierre-Yves Strub | 09 November 2021, 16:32:05 UTC | Merge pull request #88 from EasyCrypt/deploy-mu1 Consistently use `mu1` instead of `mass`. | 09 November 2021, 16:32:05 UTC |
| e770f0f | Pierre-Yves Strub | 09 November 2021, 15:36:49 UTC | Refactor & generalize the section mechanism the section mechanism has been refactored s.t. it provides a more uniform interface where any kind of declaration can be marked as local / declared and erased / generalized when the section is closed. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 09 November 2021, 15:36:49 UTC |
| 89fea98 | Pierre-Yves Strub | 08 November 2021, 15:40:18 UTC | api for tc resolution + inclusion in EcUnify | 08 November 2021, 15:40:18 UTC |
| 1fab9ba | Antoine Séré | 08 November 2021, 14:18:53 UTC | Added everything again | 08 November 2021, 14:18:53 UTC |
| b0e609d | Pierre-Yves Strub | 05 November 2021, 15:07:43 UTC | Fix the pretty printing of \ as a binop fix #93 | 05 November 2021, 15:08:07 UTC |
| a420ad5 | Pierre-Yves Strub | 05 November 2021, 10:55:18 UTC | check parent constraint when adding a new tc instance | 05 November 2021, 10:55:18 UTC |
| c2ed9ae | Pierre-Yves Strub | 05 November 2021, 10:43:22 UTC | ask for tc axioms realization when declaring an instance | 05 November 2021, 10:43:33 UTC |
| 6432c4c | Pierre-Yves Strub | 18 October 2021, 06:02:16 UTC | | 05 November 2021, 10:43:33 UTC |
| 0bae431 | Pierre-Yves Strub | 11 October 2021, 15:23:24 UTC | | 05 November 2021, 10:43:33 UTC |
| 6b79bbb | Antoine Séré | 05 November 2021, 09:43:35 UTC | Added everything | 05 November 2021, 09:43:35 UTC |
| b37085c | Christian Doczkal | 04 November 2021, 14:52:23 UTC | renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE | 04 November 2021, 14:56:36 UTC |
| d5d3d94 | Christian Doczkal | 24 October 2021, 10:45:16 UTC | adapt to consistent use of mu1 | 04 November 2021, 12:09:30 UTC |
| 6676710 | Christian Doczkal | 24 October 2021, 09:36:02 UTC | use mu1 instead of mass in in Distr | 04 November 2021, 12:06:45 UTC |
| b9c7685 | Christian Doczkal | 03 November 2021, 15:28:23 UTC | comments, renaming, proof* | 04 November 2021, 10:00:49 UTC |
| 4da60d2 | Christian Doczkal | 03 November 2021, 15:06:57 UTC | allow sdist-distinguishers for ROs to call sample and set | 04 November 2021, 10:00:49 UTC |
| 8a26fe5 | Christian Doczkal | 03 November 2021, 12:25:10 UTC | some more simplifications | 04 November 2021, 10:00:49 UTC |
| 6851729 | Christian Doczkal | 01 November 2021, 10:09:10 UTC | remove weight equality side conditions | 04 November 2021, 10:00:49 UTC |
| a21c135 | Christian Doczkal | 22 October 2021, 14:33:38 UTC | implement feedback from review | 04 November 2021, 10:00:49 UTC |
| 570f090 | Christian Doczkal | 21 October 2021, 15:48:19 UTC | fix compilation | 04 November 2021, 10:00:49 UTC |
| 7fcfa1d | Christian Doczkal | 21 October 2021, 14:21:07 UTC | move lemmas from SDist to RealSeries and Distr, rename summableM | 04 November 2021, 10:00:49 UTC |
| f1d2f19 | Christian Doczkal | 21 October 2021, 09:05:24 UTC | use PROM rather than ROM | 04 November 2021, 10:00:49 UTC |
| 051cb1d | Christian Doczkal | 20 October 2021, 15:24:05 UTC | sdist for ROM distinguishers and N distinct queries | 04 November 2021, 10:00:49 UTC |
| f5d072e | Christian Doczkal | 19 October 2021, 17:49:56 UTC | reduction from N to 1 oracle call for sdist distinguisher | 04 November 2021, 10:00:49 UTC |
| 3adc9c8 | Christian Doczkal | 18 October 2021, 16:11:21 UTC | sdist distinguisher for single oracle call + reduction to single sampling | 04 November 2021, 10:00:49 UTC |
| 62e1ce7 | Christian Doczkal | 14 October 2021, 12:55:45 UTC | connection between sdist and distinguisher procedures | 04 November 2021, 10:00:49 UTC |
| 4529cfc | Christian Doczkal | 12 October 2021, 12:10:25 UTC | statitical distance and some lemmas | 04 November 2021, 10:00:49 UTC |
| aa6dc07 | Pierre-Yves Strub | 19 October 2021, 10:19:36 UTC | Add a simple form of pattern selection in rewrite rules Syntax is: `rewrite [pattern]rule` In this form, `pattern` is first searched against the current goal and rule LHS is then matched against the instanciated pattern. E.g. `rewrite [y+_]addrC` will instantiate `addrC` to `y` and `z` assuming that the first match of `y+_` in the current goal is `y+z`. This syntax is compatible with other variants: `rewrite -{2}[y+_]addrC` | 19 October 2021, 10:19:36 UTC |
| 4afdfe9 | Pierre-Yves Strub | 18 October 2021, 12:51:49 UTC | change "smt in rewrite" syntax New syntax is: - rewrite #smt - rewrite #smt:(db) - rewrite #smt:[options] | 18 October 2021, 12:52:42 UTC |
| 7b8aa43 | Pierre-Yves Strub | 18 October 2021, 08:03:55 UTC | Compute free program variables in *hoare statements. Fix #83 | 18 October 2021, 08:03:55 UTC |
| c854989 | Pierre-Yves Strub | 12 October 2021, 13:39:31 UTC | Implement "gen have" & "wlog suff" Fix #77 | 12 October 2021, 13:39:31 UTC |
| c132a25 | Pierre-Yves Strub | 08 October 2021, 12:09:27 UTC | StdLib: summability of partitioning | 08 October 2021, 12:09:35 UTC |
| 3ffc3be | Alley Stoughton | 06 October 2021, 15:00:49 UTC | Some lemmas for floor and ceil, in particular letting one rewrite floor x and ceil x. | 07 October 2021, 06:39:26 UTC |
| d229960 | Antoine Séré | 05 October 2021, 16:07:58 UTC | Pre checkout | 05 October 2021, 16:07:58 UTC |
| 0656ac7 | Alley Stoughton | 01 October 2021, 17:11:23 UTC | Added disjoint xs ys as an abbreviation for xs `&` ys = fset0. Added lemma disjointP (xs ys : 'a fset): disjoint xs ys <=> forall (x : 'a), x \in xs => ! x \in ys. | 04 October 2021, 07:24:14 UTC |
| 64d401f | Antoine Séré | 20 September 2021, 10:19:27 UTC | Added error message when different number of type arguments in typeclass | 20 September 2021, 10:19:27 UTC |
| d5beecf | Antoine Séré | 16 September 2021, 15:13:01 UTC | Pierre-Yves fixed parser and other stuff | 16 September 2021, 15:13:01 UTC |
| ad321e5 | Antoine Séré | 16 September 2021, 13:45:30 UTC | It compiles, need to modify parser | 16 September 2021, 13:45:30 UTC |
| 51e9f8d | Antoine Séré | 16 September 2021, 12:58:20 UTC | Parser error | 16 September 2021, 12:58:20 UTC |
| 37ed00f | Antoine Séré | 13 September 2021, 16:35:38 UTC | It compiles | 13 September 2021, 16:35:38 UTC |
| 37892ab | Pierre-Yves Strub | 07 September 2021, 13:49:14 UTC | parsing entry for tc parameters | 07 September 2021, 13:49:14 UTC |
| 18abf81 | Pierre-Yves Strub | 07 September 2021, 12:40:26 UTC | Merge branch '1.0' into deploy-tc | 07 September 2021, 12:40:26 UTC |
| c07e880 | Pierre-Yves Strub | 06 September 2021, 09:47:40 UTC | Fix global positions reporting | 06 September 2021, 09:47:40 UTC |
| a8975fc | Pierre-Yves Strub | 06 July 2021, 14:16:22 UTC | TC: examples for subtypes | 06 July 2021, 14:16:22 UTC |
| 512f0f2 | François Dupressoir | 30 June 2021, 14:43:29 UTC | [docker] get CVC4 from a more stable URL | 30 June 2021, 14:43:36 UTC |
