| 84c2618 | Pierre-Yves Strub | 08 April 2021, 13:48:16 UTC | Fix stdlib | 08 April 2021, 13:48:16 UTC |
| a014668 | Pierre-Yves Strub | 08 April 2021, 13:14:10 UTC | StdLib: enumerating polynomials of a given degree | 08 April 2021, 13:14:10 UTC |
| 0a6485a | Pierre-Yves Strub | 08 April 2021, 13:13:54 UTC | StdLib: Finite: explicit witnesses for finitness + related lemmas on lists | 08 April 2021, 13:13:54 UTC |
| 81cd929 | Pierre-Yves Strub | 08 April 2021, 13:13:27 UTC | Stdlib: IntDiv - add a few lemmas | 08 April 2021, 13:13:27 UTC |
| 18e7bf4 | Pierre-Yves Strub | 08 April 2021, 07:15:49 UTC | Stdlib: more results on polynomials & ring ideals | 08 April 2021, 07:15:49 UTC |
| 83e39fd | Pierre-Yves Strub | 07 April 2021, 14:44:27 UTC | Prove that polynomials form an integral domain | 07 April 2021, 14:44:27 UTC |
| 6ce66c7 | Pierre-Yves Strub | 07 April 2021, 14:44:12 UTC | Include ring quotients th. in ideals th. | 07 April 2021, 14:44:12 UTC |
| de2158b | Pierre-Yves Strub | 07 April 2021, 12:32:34 UTC | Poly.ec -> Poly.eca | 07 April 2021, 12:32:34 UTC |
| a62a90d | Pierre-Yves Strub | 05 April 2021, 09:08:22 UTC | Stdlib: ring quotients | 05 April 2021, 09:08:22 UTC |
| cf1eca8 | Pierre-Yves Strub | 05 April 2021, 06:43:18 UTC | Stdlib: fmin | 05 April 2021, 06:43:18 UTC |
| 1aab7a8 | Pierre-Yves Strub | 05 April 2021, 06:42:55 UTC | Quotient: use std def. of eqv relation | 05 April 2021, 06:42:55 UTC |
| 2a8554f | Pierre-Yves Strub | 05 April 2021, 06:37:07 UTC | Stdlib: simplify proofs in Quotient.ec | 05 April 2021, 06:37:07 UTC |
| c404a43 | Pierre-Yves Strub | 05 April 2021, 05:51:11 UTC | Stdlib: ideas & a bit of abstract arithmetic | 05 April 2021, 05:51:11 UTC |
| 940fa12 | Pierre-Yves Strub | 05 April 2021, 05:40:35 UTC | List: fix admitted proofs | 05 April 2021, 05:40:35 UTC |
| c5d0c62 | Pierre-Yves Strub | 05 April 2021, 05:39:57 UTC | List: size_eq1 | 05 April 2021, 05:39:57 UTC |
| 432c181 | Pierre-Yves Strub | 04 April 2021, 17:54:08 UTC | README: fix why3 config command | 04 April 2021, 17:54:08 UTC |
| 748c9ef | Pierre-Yves Strub | 04 April 2021, 09:00:54 UTC | remove doc-box | 04 April 2021, 09:00:54 UTC |
| a0a0c9b | Pierre-Yves Strub | 04 April 2021, 07:17:16 UTC | Upgrade versions of supported provers | 04 April 2021, 07:17:16 UTC |
| 20a6183 | Pierre-Yves Strub | 04 April 2021, 06:42:50 UTC | Move to Why3 1.4 | 04 April 2021, 06:42:50 UTC |
| fb59000 | Pierre-Yves Strub | 03 April 2021, 19:32:58 UTC | CI: use workflow conclusion | 03 April 2021, 19:32:58 UTC |
| 7627a75 | Pierre-Yves Strub | 03 April 2021, 17:32:12 UTC | Move to GitHub Actions | 03 April 2021, 17:32:12 UTC |
| 8bcb1ae | Pierre-Yves Strub | 03 April 2021, 15:30:26 UTC | easycrypt.png | 03 April 2021, 15:30:26 UTC |
| df9ab35 | Pierre-Yves Strub | 02 April 2021, 20:27:10 UTC | Stdlib: refactoring | 02 April 2021, 20:27:10 UTC |
| 91479fa | Pierre-Yves Strub | 02 April 2021, 20:24:48 UTC | Stdlib: integer log. | 02 April 2021, 20:24:48 UTC |
| e8e6dc4 | Pierre-Yves Strub | 02 April 2021, 12:25:47 UTC | List: alltuples & allsubtuples | 02 April 2021, 12:25:47 UTC |
| 9c741f1 | Pierre-Yves Strub | 02 April 2021, 11:52:49 UTC | List: subseqs | 02 April 2021, 11:52:49 UTC |
| 30b7cae | Pierre-Yves Strub | 02 April 2021, 07:28:20 UTC | Finite types pred + finfun. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 02 April 2021, 07:28:20 UTC |
| f2abfb4 | Francois Dupressoir | 30 March 2021, 14:59:52 UTC | Merge pull request #60 from EasyCrypt/deploy-no-eco Add a -no-eco option to disable .eco generation | 30 March 2021, 14:59:52 UTC |
| 3a626d5 | François Dupressoir | 30 March 2021, 13:09:44 UTC | Add a -no-eco option to disable .eco generation Existing .eco cached results are used, but new ones are not generated | 30 March 2021, 13:09:44 UTC |
| c57f05e | François Dupressoir | 25 March 2021, 16:47:12 UTC | Proper goal for conseq equiv hoare => hoare. | 25 March 2021, 17:04:40 UTC |
| 98608e4 | Benjamin Gregoire | 24 March 2021, 03:41:53 UTC | fix translation to why3 for operator, where some of its type parameters do not appear in the its type. | 24 March 2021, 03:41:53 UTC |
| f5ea5b3 | Francois Dupressoir | 17 March 2021, 15:55:39 UTC | Fix supported alt-ergo version Not that this will be valid very long... | 17 March 2021, 15:55:39 UTC |
| 4818c2e | Francois Dupressoir | 17 March 2021, 14:04:26 UTC | Document why3/prover version interactions | 17 March 2021, 14:04:26 UTC |
| ddb426b | Alley Stoughton | 16 March 2021, 16:39:12 UTC | Removing dead code. | 16 March 2021, 16:39:12 UTC |
| c19a2a7 | Pierre-Yves Strub | 03 March 2021, 14:07:57 UTC | remove debugging informations | 03 March 2021, 14:07:57 UTC |
| d6e792c | Pierre-Yves Strub | 02 March 2021, 19:46:05 UTC | tactic/if: do not eagerly simplfy the pre fix #52 | 02 March 2021, 19:47:13 UTC |
| 82b7089 | Pierre-Yves Strub | 25 February 2021, 11:46:34 UTC | refactoring proofs | 25 February 2021, 11:46:34 UTC |
| d2e0537 | Benjamin Gregoire | 25 February 2021, 10:29:19 UTC | more lemma on dbfun | 25 February 2021, 10:29:19 UTC |
| b2bc4e8 | Benjamin Gregoire | 25 February 2021, 03:37:03 UTC | add lemma dfun_ll | 25 February 2021, 03:37:03 UTC |
| e0e995f | Pierre-Yves Strub | 24 February 2021, 23:34:31 UTC | stdlib: eager biased sampling | 24 February 2021, 23:34:31 UTC |
| f4debca | Pierre-Yves Strub | 24 February 2021, 21:37:09 UTC | stdlib: more results on dfun | 24 February 2021, 21:37:09 UTC |
| 7a60dcc | Pierre-Yves Strub | 24 February 2021, 13:00:54 UTC | stdlib: gen. def. of distr. of functions | 24 February 2021, 13:00:54 UTC |
| a7ca8c7 | Pierre-Yves Strub | 02 February 2021, 14:18:43 UTC | Lib: uniform distributions over finite functions | 02 February 2021, 14:18:43 UTC |
| 708e88c | Pierre-Yves Strub | 16 January 2021, 08:38:18 UTC | Losslessness axioms are now added to the "rnd" database | 16 January 2021, 08:38:18 UTC |
| 9dcb1a4 | Pierre-Yves Strub | 16 January 2021, 07:53:24 UTC | Renaming: XXX_full -> XXX_fu | 16 January 2021, 07:53:35 UTC |
| 7314a12 | Benjamin Gregoire | 16 January 2021, 05:42:38 UTC | printing added lemma by operator declaration | 16 January 2021, 05:43:39 UTC |
| f7e2b19 | Pierre-Yves Strub | 15 January 2021, 14:03:21 UTC | Basic results on dvector/dmatrix | 15 January 2021, 14:03:21 UTC |
| b5f65bc | Pierre-Yves Strub | 15 January 2021, 09:29:53 UTC | Basic results on dvector/dmatrix | 15 January 2021, 09:29:53 UTC |
| 844e61b | Pierre-Yves Strub | 15 January 2021, 08:11:01 UTC | More results on dlet/dmap | 15 January 2021, 08:11:01 UTC |
| bb0a97a | Pierre-Yves Strub | 13 January 2021, 15:15:47 UTC | Axiomatized operators are now forcibly unfoldable | 13 January 2021, 15:15:47 UTC |
| 88e05a0 | Benjamin Gregoire | 12 January 2021, 14:55:42 UTC | t_subst not in the trusted base + some improvement to />. | 12 January 2021, 14:55:42 UTC |
| 5583bca | Benjamin Gregoire | 12 January 2021, 14:15:46 UTC | pragma -oldip become the default | 12 January 2021, 14:15:46 UTC |
| 6feb5d7 | Benjamin Gregoire | 05 January 2021, 11:47:23 UTC | fix quadratic behavior of ecCallbyValue | 05 January 2021, 11:47:23 UTC |
| 999561c | Pierre-Yves Strub | 04 January 2021, 13:24:41 UTC | remove deprecated "cut" tactic | 04 January 2021, 13:24:41 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 |
| 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 |
| 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 |
| 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 |
| 19c7285 | Pierre-Yves Strub | 20 October 2020, 09:34:40 UTC | New operator: dfold | 20 October 2020, 09:40:14 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 |
| 7ba9ba4 | Pierre-Yves Strub | 11 October 2020, 07:27:44 UTC | Docker image: bump provers versions | 11 October 2020, 07:27:44 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 |
| 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 |
