| 3a2ef0e | Pierre-Yves Strub | 11 January 2021, 14:04:57 UTC | Add debug mark | 11 January 2021, 14:04:57 UTC |
| 3b66108 | Pierre-Yves Strub | 05 January 2021, 12:53:49 UTC | Merge branch '1.0' into 1.0-preview | 05 January 2021, 12:53:49 UTC |
| 6feb5d7 | Benjamin Gregoire | 05 January 2021, 11:47:23 UTC | fix quadratic behavior of ecCallbyValue | 05 January 2021, 11:47:23 UTC |
| 92f57b4 | Pierre-Yves Strub | 04 January 2021, 13:25:09 UTC | Merge branch '1.0' into 1.0-preview | 04 January 2021, 13:25:09 UTC |
| 999561c | Pierre-Yves Strub | 04 January 2021, 13:24:41 UTC | remove deprecated "cut" tactic | 04 January 2021, 13:24:41 UTC |
| cb4def3 | Pierre-Yves Strub | 04 January 2021, 10:39:56 UTC | Merge branch '1.0' into 1.0-preview | 04 January 2021, 10:39:56 UTC |
| f4f3f94 | Pierre-Yves Strub | 04 January 2021, 10:26:56 UTC | implement -R flag | 04 January 2021, 10:26:56 UTC |
| 3671d46 | Pierre-Yves Strub | 18 December 2020, 20:07:48 UTC | Travis -> CircleCI | 18 December 2020, 20:07:48 UTC |
| 35e59d1 | Pierre-Yves Strub | 04 December 2020, 14:05:15 UTC | `apply` is now using product-compatible matching | 04 December 2020, 14:05:15 UTC |
| 6504b04 | Pierre-Yves Strub | 03 December 2020, 13:54:55 UTC | remove debug infos | 03 December 2020, 13:55:10 UTC |
| 3c14f4d | Benjamin Gregoire | 03 December 2020, 07:08:30 UTC | small refactoring | 03 December 2020, 07:08:30 UTC |
| 177f61d | Benjamin Gregoire | 03 December 2020, 05:53:30 UTC | add trivial lemma | 03 December 2020, 05:53:30 UTC |
| e7ca052 | Benjamin Gregoire | 02 December 2020, 15:08:03 UTC | stack based conversion | 02 December 2020, 15:08:03 UTC |
| 93748b3 | Pierre-Yves Strub | 01 December 2020, 09:41:56 UTC | Decimal numbers are now translated to irreducible fractions | 01 December 2020, 09:41:56 UTC |
| de9fdea | Pierre-Yves Strub | 01 December 2020, 08:48:33 UTC | In pose/trivial: use less conversion, cleanup chain of trivial calls. | 01 December 2020, 08:48:33 UTC |
| 68b3ffa | Benjamin Gregoire | 27 November 2020, 16:47:34 UTC | make congr less costly | 27 November 2020, 16:47:34 UTC |
| ea13c71 | Benjamin Gregoire | 27 November 2020, 16:46:54 UTC | simplify t_split | 27 November 2020, 16:46:54 UTC |
| 2363562 | Benjamin Gregoire | 24 November 2020, 19:47:13 UTC | fix cbv user_red | 24 November 2020, 19:47:13 UTC |
| bf76f88 | Alley Stoughton | 24 November 2020, 16:20:22 UTC | [fix #17390] | 24 November 2020, 16:20:22 UTC |
| 6857723 | Benjamin Gregoire | 24 November 2020, 13:48:55 UTC | simplify user reduction | 24 November 2020, 13:49:28 UTC |
| fcdfcbd | Pierre-Yves Strub | 21 November 2020, 12:11:49 UTC | Core theory for univariate polynomials | 21 November 2020, 12:11:49 UTC |
| a08bc34 | Pierre-Yves Strub | 21 November 2020, 08:29:35 UTC | Stdlib: more results on Rn + bigops on Rn | 21 November 2020, 08:29:35 UTC |
| 7a42484 | Pierre-Yves Strub | 21 November 2020, 00:14:50 UTC | MANIFEST | 21 November 2020, 00:14:50 UTC |
| 07b937c | Pierre-Yves Strub | 20 November 2020, 22:16:40 UTC | Small addititions on distributions | 20 November 2020, 22:16:40 UTC |
| 6f68e27 | Pierre-Yves Strub | 20 November 2020, 14:45:54 UTC | More results on distributions (conditional exp, Jensen (finite)) | 20 November 2020, 14:45:54 UTC |
| e002644 | Alley Stoughton | 20 November 2020, 08:05:03 UTC | When a match has duplicate constructors but the same number of (#47) branches as the number of constructors in the datatype being matched, an exception was raised instead of the expected error message being issued. Example: type t = [A | B]. module M = { proc f(x : t) = { match x with | A => { } | A => { } end; } }. | 20 November 2020, 08:05:03 UTC |
| 27ff637 | Pierre-Yves Strub | 18 November 2020, 06:00:50 UTC | integrating more results on distributions | 18 November 2020, 06:00:50 UTC |
| 8d01a80 | Benjamin Gregoire | 17 November 2020, 17:48:08 UTC | fix CBC | 17 November 2020, 17:48:08 UTC |
| ed25190 | Benjamin Gregoire | 16 November 2020, 10:58:31 UTC | small generalization of PRP | 16 November 2020, 10:58:31 UTC |
| 8cb3e88 | Benjamin Gregoire | 13 November 2020, 11:33:30 UTC | extend conseq rules: equivF => hoareF => hoareF and equivF => phoareF => phoareF | 13 November 2020, 11:33:47 UTC |
| 4391b04 | Pierre-Yves Strub | 12 November 2020, 11:00:16 UTC | basic results about minr | 12 November 2020, 11:00:16 UTC |
| 61de4b9 | Pierre-Yves Strub | 12 November 2020, 08:24:07 UTC | Fix "smt debug" | 12 November 2020, 08:24:20 UTC |
| b360fa8 | Benjamin Gregoire | 11 November 2020, 05:55:58 UTC | Fix bug in conseq | 11 November 2020, 05:56:42 UTC |
| ffad375 | Pierre-Yves Strub | 03 November 2020, 09:04:00 UTC | New option for SMT: "debug" | 03 November 2020, 09:04:00 UTC |
| 6c677e1 | Pierre-Yves Strub | 21 October 2020, 08:49:57 UTC | Merge branch '1.0' into 1.0-preview | 21 October 2020, 08:49:57 UTC |
| 4ef4286 | Pierre-Yves Strub | 21 October 2020, 08:49:24 UTC | Fix dfold s.t. the functor takes the index | 21 October 2020, 08:49:24 UTC |
| b6ad2d5 | Pierre-Yves Strub | 20 October 2020, 09:40:43 UTC | Merge branch '1.0' into 1.0-preview | 20 October 2020, 09:40:43 UTC |
| 19c7285 | Pierre-Yves Strub | 20 October 2020, 09:34:40 UTC | New operator: dfold | 20 October 2020, 09:40:14 UTC |
| 0049a66 | Pierre-Yves Strub | 15 October 2020, 10:30:04 UTC | README (nix) | 20 October 2020, 09:35:00 UTC |
| 907c61f | Pierre-Yves Strub | 15 October 2020, 08:39:16 UTC | "={_}" now supports the construction "glob M \ { p1, p2, ... }" It stands for "glob M" without "p1, p2, ..." | 20 October 2020, 09:34:59 UTC |
| c55c6d8 | Pierre-Yves Strub | 14 October 2020, 09:10:10 UTC | better printing of modules bodies w.r.t. "import var" | 20 October 2020, 09:34:59 UTC |
| 178431c | Pierre-Yves Strub | 14 October 2020, 07:08:46 UTC | The command "import var" is now allowed at top-level | 20 October 2020, 09:34:59 UTC |
| aba1306 | Pierre-Yves Strub | 14 October 2020, 06:55:56 UTC | add alias "include var" that stands for "include" then "import var" | 20 October 2020, 09:34:59 UTC |
| 0b19b59 | Pierre-Yves Strub | 14 October 2020, 06:52:22 UTC | "import var" now takes a space-separated list of modules | 20 October 2020, 09:34:59 UTC |
| bd02fdb | Pierre-Yves Strub | 14 October 2020, 06:33:40 UTC | New command in modules: import var M This imports the variables of M in the active module scope. | 20 October 2020, 09:34:59 UTC |
| c987761 | Pierre-Yves Strub | 11 October 2020, 07:27:44 UTC | Docker image: bump provers versions | 20 October 2020, 09:34:59 UTC |
| fa3853d | Pierre-Yves Strub | 15 October 2020, 10:30:04 UTC | README (nix) | 15 October 2020, 10:30:04 UTC |
| bc4f6df | Pierre-Yves Strub | 15 October 2020, 08:39:16 UTC | "={_}" now supports the construction "glob M \ { p1, p2, ... }" It stands for "glob M" without "p1, p2, ..." | 15 October 2020, 08:39:16 UTC |
| 22a8b51 | Pierre-Yves Strub | 14 October 2020, 09:10:10 UTC | better printing of modules bodies w.r.t. "import var" | 14 October 2020, 09:10:10 UTC |
| ca1f0d2 | Pierre-Yves Strub | 14 October 2020, 07:08:46 UTC | The command "import var" is now allowed at top-level | 14 October 2020, 07:08:46 UTC |
| b34c174 | Pierre-Yves Strub | 14 October 2020, 06:55:56 UTC | add alias "include var" that stands for "include" then "import var" | 14 October 2020, 06:55:56 UTC |
| c3114bd | Pierre-Yves Strub | 14 October 2020, 06:52:22 UTC | "import var" now takes a space-separated list of modules | 14 October 2020, 06:52:22 UTC |
| 4268b0f | Pierre-Yves Strub | 14 October 2020, 06:33:40 UTC | New command in modules: import var M This imports the variables of M in the active module scope. | 14 October 2020, 06:34:14 UTC |
| 66784bc | Vitor Pereira | 12 October 2020, 23:02:09 UTC | Merge branch '1.0-preview' of https://github.com/EasyCrypt/easycrypt into HEAD | 12 October 2020, 23:02:09 UTC |
| 97ebd49 | Vitor Pereira | 12 October 2020, 23:00:34 UTC | version update | 12 October 2020, 23:00:34 UTC |
| 7ba9ba4 | Pierre-Yves Strub | 11 October 2020, 07:27:44 UTC | Docker image: bump provers versions | 11 October 2020, 07:27:44 UTC |
| f8ea221 | François Dupressoir | 10 October 2020, 12:10:17 UTC | Merge branch '1.0' into 1.0-preview | 10 October 2020, 12:10:17 UTC |
| 7d8a513 | François Dupressoir | 10 October 2020, 11:22:49 UTC | Help smt along in brittle proofs These SMT fail when using: - Why3 1.3.1 - Z3 4.8.9 - CVC4 1.9 - Alt-Ergo 1.3.3 This appears to be bad interplay between the provers and this version of Why3: the proofs work with Why3 1.2 | 10 October 2020, 12:08:14 UTC |
| 221e1b2 | François Dupressoir | 10 October 2020, 10:47:31 UTC | Merge branch '1.0' into 1.0-preview | 10 October 2020, 10:47:31 UTC |
| 933e315 | Pierre-Yves Strub | 10 October 2020, 10:34:11 UTC | Merge branch '1.0' into 1.0-preview | 10 October 2020, 10:34:11 UTC |
| 469a12a | François Dupressoir | 09 October 2020, 16:20:54 UTC | easycrypt why3config uses --full-config | 09 October 2020, 16:20:54 UTC |
| ef6f0ba | Pierre-Yves Strub | 09 October 2020, 15:44:59 UTC | README: add --full-config option (why3 config) | 09 October 2020, 15:44:59 UTC |
| 6d31cc5 | Pierre-Yves Strub | 09 October 2020, 15:44:32 UTC | Update Dockerfile w.r.t new EasyCrypt repo layout | 09 October 2020, 15:44:32 UTC |
| e664da3 | Pierre-Yves Strub | 09 October 2020, 11:02:44 UTC | Docker: do not use easycrypt remote anymore | 09 October 2020, 11:02:44 UTC |
| ce70fa4 | Pierre-Yves Strub | 09 October 2020, 10:23:24 UTC | opam: change post-install message | 09 October 2020, 10:23:24 UTC |
| 6c03840 | Pierre-Yves Strub | 09 October 2020, 10:21:16 UTC | Fix travis configuration file w.r.t recent changes | 09 October 2020, 10:21:16 UTC |
| 44a728a | Pierre-Yves Strub | 09 October 2020, 10:16:24 UTC | Update README (no more external opam repo) & add missing opam fields | 09 October 2020, 10:16:58 UTC |
| e37a10c | Pierre-Yves Strub | 09 October 2020, 08:12:15 UTC | Import opam file s.t. travis can use it to update its dependencies | 09 October 2020, 08:41:05 UTC |
| c436fd4 | Pierre-Yves Strub | 09 October 2020, 07:16:05 UTC | Travis: update EasyCrypt dependencies before running tests | 09 October 2020, 08:41:05 UTC |
| 730f329 | Pierre-Yves Strub | 09 October 2020, 08:02:28 UTC | default.nix: remove restriction on Why3 version | 09 October 2020, 08:41:05 UTC |
| 8f33b95 | Stephane Graham-Lengrand | 07 October 2020, 23:19:47 UTC | First attempt at handling Why3 1.3.X | 09 October 2020, 08:41:05 UTC |
| 3007982 | Benjamin Gregoire | 14 September 2020, 13:36:41 UTC | fix default.nix | 14 September 2020, 13:36:41 UTC |
| 67208f2 | Benjamin Gregoire | 09 July 2020, 12:12:20 UTC | add UC example | 09 July 2020, 12:12:20 UTC |
| 9001c68 | Adrien Koutsos | 08 July 2020, 13:22:50 UTC | minor fix | 08 July 2020, 13:22:50 UTC |
| 29332ce | Benjamin Gregoire | 08 July 2020, 13:18:24 UTC | more printing info | 08 July 2020, 13:18:31 UTC |
| a5a0242 | Benjamin Gregoire | 07 July 2020, 12:28:51 UTC | fix bug | 08 July 2020, 13:18:31 UTC |
| 374f418 | Pierre-Yves Strub | 06 July 2020, 15:12:21 UTC | fix cost examples + put them in the test suite | 06 July 2020, 15:12:21 UTC |
| ff46b20 | Adrien Koutsos | 06 July 2020, 14:17:24 UTC | removed old file | 06 July 2020, 14:17:44 UTC |
| 37b3bb3 | Benjamin Gregoire | 06 July 2020, 14:06:24 UTC | fix wp with match | 06 July 2020, 14:07:22 UTC |
| cec9b3b | Adrien Koutsos | 06 July 2020, 13:15:29 UTC | started cleaning-up the small tutorial | 06 July 2020, 13:15:29 UTC |
| 6395c43 | Adrien Koutsos | 03 July 2020, 13:07:11 UTC | minor | 03 July 2020, 13:07:11 UTC |
| 685ba77 | Adrien Koutsos | 03 July 2020, 13:02:49 UTC | check convertibility when sub-typing | 03 July 2020, 13:03:13 UTC |
| 9559218 | Benjamin Gregoire | 29 June 2020, 12:04:27 UTC | use xint in cost | 29 June 2020, 12:04:27 UTC |
| d87925d | Benjamin Gregoire | 25 June 2020, 06:33:37 UTC | add opp | 25 June 2020, 06:33:46 UTC |
| 3bd48b4 | Pierre-Yves Strub | 24 June 2020, 15:35:12 UTC | more lemmas | 24 June 2020, 15:35:12 UTC |
| e18752e | Benjamin Gregoire | 24 June 2020, 15:14:42 UTC | all examples work | 24 June 2020, 15:15:08 UTC |
| 356fcac | Benjamin Gregoire | 24 June 2020, 15:02:47 UTC | some cleanup | 24 June 2020, 15:15:08 UTC |
| e571b4d | Benjamin Gregoire | 24 June 2020, 14:51:19 UTC | fix tactics and examples | 24 June 2020, 15:15:08 UTC |
| a4fb2e3 | Pierre-Yves Strub | 24 June 2020, 13:10:51 UTC | xint | 24 June 2020, 13:10:51 UTC |
| 416b59b | Pierre-Yves Strub | 24 June 2020, 10:14:36 UTC | xint typwe | 24 June 2020, 10:14:36 UTC |
| cdef8e7 | Benjamin Gregoire | 23 June 2020, 13:01:23 UTC | more on examples | 23 June 2020, 13:01:23 UTC |
| 5b2759d | Benjamin Gregoire | 23 June 2020, 13:01:07 UTC | fix abstract proc rule | 23 June 2020, 13:01:07 UTC |
| 41c4faf | Benjamin Gregoire | 22 June 2020, 13:48:18 UTC | fix tactic if for choare | 22 June 2020, 13:48:18 UTC |
| bc4a801 | Benjamin Gregoire | 22 June 2020, 13:47:36 UTC | fix reduction and conversion for quantification over modules | 22 June 2020, 13:47:36 UTC |
| 3c4d4be | Benjamin Gregoire | 22 June 2020, 13:45:43 UTC | fix syntax | 22 June 2020, 13:46:42 UTC |
| 095eeff | Benjamin Gregoire | 22 June 2020, 07:35:59 UTC | Fix big in convertion | 22 June 2020, 07:35:59 UTC |
| 24212dd | Benjamin Gregoire | 20 June 2020, 06:34:48 UTC | complexity proof for indcpa-1 indcpa-n almost finish | 20 June 2020, 06:34:48 UTC |
| b28d149 | Benjamin Gregoire | 20 June 2020, 06:33:57 UTC | more uniform syntaxe | 20 June 2020, 06:33:57 UTC |
| f03e44b | Benjamin Gregoire | 20 June 2020, 06:33:27 UTC | fix automatique part of if rule for choareS | 20 June 2020, 06:33:27 UTC |
| 63d5932 | Benjamin Gregoire | 20 June 2020, 06:32:25 UTC | fix env for proc rule in choare | 20 June 2020, 06:32:25 UTC |
