| 40e5e97 | Adrien Koutsos | 04 November 2021, 17:08:31 UTC | [WIP] | 04 November 2021, 17:08:31 UTC |
| 1b8c136 | Adrien Koutsos | 04 November 2021, 09:43:30 UTC | [WIP] | 04 November 2021, 09:43:30 UTC |
| 8d8a607 | Adrien Koutsos | 03 November 2021, 13:43:43 UTC | [WIP] | 03 November 2021, 17:54:56 UTC |
| 9c99185 | Adrien Koutsos | 03 November 2021, 11:29:21 UTC | [WIP] | 03 November 2021, 11:29:21 UTC |
| f708b3c | Adrien Koutsos | 03 November 2021, 09:24:00 UTC | [WIP] | 03 November 2021, 09:24:00 UTC |
| f59c30a | Adrien Koutsos | 02 November 2021, 17:35:37 UTC | [WIP] | 02 November 2021, 17:35:37 UTC |
| ea15b69 | Adrien Koutsos | 02 November 2021, 13:53:21 UTC | [WIP] | 02 November 2021, 13:53:21 UTC |
| 26374f9 | Adrien Koutsos | 02 November 2021, 13:53:09 UTC | [WIP] | 02 November 2021, 13:53:09 UTC |
| 62c5688 | Adrien Koutsos | 07 October 2021, 16:32:27 UTC | [WIP] | 07 October 2021, 16:32:27 UTC |
| ab7ee1d | Adrien Koutsos | 07 October 2021, 15:59:24 UTC | [WIP] | 07 October 2021, 15:59:24 UTC |
| 431396d | Adrien Koutsos | 07 October 2021, 12:27:31 UTC | added cost vectors to the parser | 07 October 2021, 12:27:31 UTC |
| aabd8df | Adrien Koutsos | 07 October 2021, 09:56:50 UTC | added Fol.Fcost and Types.Tcost | 07 October 2021, 09:56:50 UTC |
| 2f4748b | Adrien Koutsos | 28 June 2021, 13:55:18 UTC | small refactoring | 04 October 2021, 09:15:27 UTC |
| b40d073 | Adrien Koutsos | 28 June 2021, 12:17:13 UTC | fixed PKE | 28 June 2021, 12:17:13 UTC |
| 153a72c | Adrien Koutsos | 28 June 2021, 12:08:43 UTC | fixed br93 | 28 June 2021, 12:08:43 UTC |
| 84e9ae6 | Adrien Koutsos | 28 June 2021, 11:58:46 UTC | fixed typing bug | 28 June 2021, 11:58:46 UTC |
| b14d514 | Adrien Koutsos | 28 June 2021, 11:47:18 UTC | fixed reduction with new cost | 28 June 2021, 11:47:18 UTC |
| a9163fe | Adrien Koutsos | 25 June 2021, 13:27:54 UTC | two bug fix | 25 June 2021, 13:27:54 UTC |
| 1162eee | Adrien Koutsos | 25 June 2021, 12:39:42 UTC | fixed type error when adding costs | 25 June 2021, 12:39:42 UTC |
| e944a67 | Adrien Koutsos | 25 June 2021, 11:02:20 UTC | extend complexity restrictions with abstract calls | 25 June 2021, 11:02:20 UTC |
| 756285e | Adrien Koutsos | 25 June 2021, 10:29:15 UTC | starting extending complexity restrictions with abstract calls | 25 June 2021, 10:29:15 UTC |
| de927e1 | Adrien Koutsos | 24 June 2021, 15:34:35 UTC | minor example fixes | 24 June 2021, 15:34:35 UTC |
| b0b97b7 | Adrien Koutsos | 24 June 2021, 14:38:20 UTC | fixed error in trans_restr_oracle_calls | 24 June 2021, 14:38:20 UTC |
| fdda04b | Adrien Koutsos | 24 June 2021, 13:57:16 UTC | changed complexity restriction syntax | 24 June 2021, 13:57:16 UTC |
| dca328a | Adrien Koutsos | 24 June 2021, 13:53:40 UTC | shorted syntax for call rule with cost information | 24 June 2021, 13:53:53 UTC |
| 4b5dfc9 | Adrien Koutsos | 24 June 2021, 13:45:39 UTC | In the call rule, abstract oracle cases no longer require user input | 24 June 2021, 13:45:39 UTC |
| 2dab2f8 | Adrien Koutsos | 24 June 2021, 12:52:27 UTC | minor | 24 June 2021, 12:52:27 UTC |
| 25d3af3 | Adrien Koutsos | 24 June 2021, 12:52:07 UTC | added missing default case + missing error message | 24 June 2021, 12:52:07 UTC |
| 5f95cc6 | Adrien Koutsos | 23 June 2021, 09:48:59 UTC | starting to fix the tutorial + bug fixes | 23 June 2021, 11:57:31 UTC |
| 3b1ab8b | Adrien Koutsos | 22 June 2021, 11:48:33 UTC | [WIP] first compiling draft | 23 June 2021, 09:12:23 UTC |
| 1dd822e | Adrien Koutsos | 17 June 2021, 11:27:39 UTC | renamed cost_bnd into shorter c_bnd | 17 June 2021, 11:27:39 UTC |
| 7057c5a | Adrien Koutsos | 17 June 2021, 11:26:32 UTC | [WIP] change costs semantics in module restrictions and choares | 17 June 2021, 11:26:32 UTC |
| bd95a13 | Adrien Koutsos | 16 June 2021, 16:44:02 UTC | [WIP] change costs semantics in module restrictions and choares | 16 June 2021, 16:44:02 UTC |
| 6143e7e | Adrien Koutsos | 16 June 2021, 13:46:25 UTC | [WIP] change costs semantics in module restrictions and choares | 16 June 2021, 13:46:25 UTC |
| 7b10c63 | Adrien Koutsos | 15 June 2021, 16:53:34 UTC | [WIP] change costs semantics in module restrictions and choares | 15 June 2021, 16:53:34 UTC |
| eac8283 | Adrien Koutsos | 14 June 2021, 12:23:33 UTC | [WIP] change substitution of a mident | 14 June 2021, 12:23:33 UTC |
| c9b7393 | Adrien Koutsos | 02 June 2021, 13:46:03 UTC | fixed syntax change of bab83fc46 | 02 June 2021, 13:46:03 UTC |
| 7ab0146 | Adrien Koutsos | 02 June 2021, 13:45:52 UTC | fixed default.nix | 02 June 2021, 13:45:52 UTC |
| 5f1ed5a | Pierre-Yves Strub | 21 April 2021, 08:28:34 UTC | README | 21 April 2021, 08:28:34 UTC |
| bffac06 | Pierre-Yves Strub | 14 April 2021, 16:29:23 UTC | Merge branch '1.0-preview' into deploy-cost-1.0-preview | 14 April 2021, 16:29:23 UTC |
| 8b8fe79 | Pierre-Yves Strub | 14 April 2021, 15:58:55 UTC | Merge branch '1.0' into 1.0-preview | 14 April 2021, 15:58:55 UTC |
| 2afb775 | Pierre-Yves Strub | 14 April 2021, 15:27:25 UTC | StdLib: funi + same weight => eq | 14 April 2021, 15:27:25 UTC |
| 5df6a6f | Pierre-Yves Strub | 13 April 2021, 13:34:33 UTC | StdLib: basic facts on distributions | 13 April 2021, 13:34:33 UTC |
| 1b25ed4 | Pierre-Yves Strub | 12 April 2021, 09:31:13 UTC | Fix bug in theory renamings | 12 April 2021, 09:31:13 UTC |
| 40d1950 | Pierre-Yves Strub | 12 April 2021, 06:10:36 UTC | StdLib: ZModP: finite + uniform distribution | 12 April 2021, 06:10:36 UTC |
| 7ad9727 | Pierre-Yves Strub | 11 April 2021, 13:06:28 UTC | StdLib: linking sampling in Z/pZ and Z/qZ when q|p | 11 April 2021, 13:06:28 UTC |
| c6ad4b1 | Pierre-Yves Strub | 10 April 2021, 14:05:38 UTC | StdLib: Poly: killing last admits | 10 April 2021, 14:05:38 UTC |
| 81f358d | Pierre-Yves Strub | 10 April 2021, 10:47:47 UTC | StdLib: polynomials distributions | 10 April 2021, 10:47:47 UTC |
| 639a76e | Pierre-Yves Strub | 09 April 2021, 20:10:53 UTC | StdLib: lead coeff. and degree of X^n+1 | 09 April 2021, 20:10:53 UTC |
| 8e6dd9a | Pierre-Yves Strub | 09 April 2021, 18:16:22 UTC | StdLib: ring quotient for non-integral domains | 09 April 2021, 18:16:22 UTC |
| 6a4bbab | Pierre-Yves Strub | 09 April 2021, 16:55:55 UTC | StdLib: ring regular element + poly over non integral domains | 09 April 2021, 16:55:55 UTC |
| 9e43d2c | Pierre-Yves Strub | 09 April 2021, 15:30:53 UTC | StdLib: more results on pmin | 09 April 2021, 15:30:53 UTC |
| 7fbcff7 | Pierre-Yves Strub | 08 April 2021, 16:42:07 UTC | StdLib: few lemmas about polynomials | 08 April 2021, 16:42:07 UTC |
| 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 |
| 7a4c6d1 | Pierre-Yves Strub | 05 April 2021, 09:08:22 UTC | Stdlib: ring quotients | 06 April 2021, 05:28:48 UTC |
| e8e4349 | Pierre-Yves Strub | 05 April 2021, 06:43:18 UTC | Stdlib: fmin | 06 April 2021, 05:28:48 UTC |
| 22c656e | Pierre-Yves Strub | 05 April 2021, 06:42:55 UTC | Quotient: use std def. of eqv relation | 06 April 2021, 05:28:48 UTC |
| 4f4e165 | Pierre-Yves Strub | 05 April 2021, 06:37:07 UTC | Stdlib: simplify proofs in Quotient.ec | 06 April 2021, 05:28:48 UTC |
| 101a76d | Pierre-Yves Strub | 05 April 2021, 05:51:11 UTC | Stdlib: ideas & a bit of abstract arithmetic | 06 April 2021, 05:28:48 UTC |
| 94ac9ac | Pierre-Yves Strub | 05 April 2021, 05:40:35 UTC | List: fix admitted proofs | 06 April 2021, 05:28:48 UTC |
| 8d240f6 | Pierre-Yves Strub | 05 April 2021, 05:39:57 UTC | List: size_eq1 | 06 April 2021, 05:28:48 UTC |
| 6084e7e | Pierre-Yves Strub | 04 April 2021, 17:54:08 UTC | README: fix why3 config command | 06 April 2021, 05:28:48 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 |
| 9ff108a | Alley Stoughton | 04 April 2021, 17:44:35 UTC | Merge branch '1.0' into 1.0-preview | 04 April 2021, 17:44:35 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 |
| 66b5409 | Pierre-Yves Strub | 03 April 2021, 17:43:58 UTC | Merge branch '1.0' into 1.0-preview | 03 April 2021, 17:43: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 |
| bab83fc | Benjamin Gregoire | 30 March 2021, 10:25:55 UTC | simplify syntaxe of call rule | 30 March 2021, 10:25:55 UTC |
| f649eab | Benjamin Gregoire | 30 March 2021, 09:22:14 UTC | add simplification lemmas on xint | 30 March 2021, 09:22:14 UTC |
| 2e7cdcd | François Dupressoir | 25 March 2021, 16:47:12 UTC | Proper goal for conseq equiv hoare => hoare. | 26 March 2021, 12:57:04 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 |
| 3990ed8 | Benjamin Gregoire | 24 March 2021, 06:10:58 UTC | fix previous merge | 24 March 2021, 06:10:58 UTC |
| 18fa1b6 | Benjamin Gregoire | 24 March 2021, 06:08:13 UTC | Merge branch '1.0-preview' into deploy-cost-1.0-preview | 24 March 2021, 06:08:13 UTC |
| 81b28cf | Benjamin Gregoire | 24 March 2021, 05:56:58 UTC | Merge branch '1.0' into 1.0-preview | 24 March 2021, 05:56:58 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 |
