| 555d19a | Pierre-Yves Strub | 18 December 2020, 20:07:48 UTC | Travis -> CircleCI | 18 January 2021, 13:33:30 UTC |
| d5fafd9 | Stephane Graham-Lengrand | 07 October 2020, 23:19:47 UTC | First attempt at handling Why3 1.3.X | 18 January 2021, 13:31:51 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 |
| 511b677 | Adrien Koutsos | 19 June 2020, 11:54:46 UTC | allow cost precondition in rcondf, rcondt and if tactics | 19 June 2020, 12:04:57 UTC |
| 1cf2c5e | Benjamin Gregoire | 18 June 2020, 09:30:36 UTC | fix typing | 18 June 2020, 09:30:36 UTC |
| 9a69f0e | Benjamin Gregoire | 17 June 2020, 13:05:32 UTC | fix cramer-shoup | 17 June 2020, 13:05:32 UTC |
| 4ba4b70 | Benjamin Gregoire | 17 June 2020, 12:21:02 UTC | fix make check | 17 June 2020, 12:21:02 UTC |
| 4893a64 | Benjamin Gregoire | 17 June 2020, 11:54:21 UTC | add cost in library + br93 and hashed_elgamal_generic | 17 June 2020, 11:54:21 UTC |
| 270b96e | Benjamin Gregoire | 17 June 2020, 06:25:31 UTC | improve example | 17 June 2020, 06:25:31 UTC |
| b929dfa | Benjamin Gregoire | 17 June 2020, 06:25:14 UTC | improve wp for choare | 17 June 2020, 06:25:14 UTC |
| 33dcdaa | Benjamin Gregoire | 17 June 2020, 06:24:44 UTC | fix reduction for schema | 17 June 2020, 06:24:44 UTC |
| 99ee382 | Benjamin Gregoire | 16 June 2020, 17:38:35 UTC | hashed_elgamal_generic with existential and without Bound module | 16 June 2020, 17:38:35 UTC |
| b4c0a2c | Adrien Koutsos | 16 June 2020, 11:24:17 UTC | fix | 16 June 2020, 11:24:17 UTC |
| b0d3571 | Adrien Koutsos | 16 June 2020, 11:17:54 UTC | rnd with precondition for choare | 16 June 2020, 11:18:08 UTC |
| 17b26f7 | Benjamin Gregoire | 16 June 2020, 10:42:20 UTC | some progress | 16 June 2020, 10:42:20 UTC |
| 1e0f9dc | Benjamin Gregoire | 15 June 2020, 15:49:32 UTC | improve hashed_elgamal_std | 15 June 2020, 15:49:32 UTC |
| e5ce65c | Benjamin Gregoire | 15 June 2020, 13:54:30 UTC | complexity | 15 June 2020, 13:54:30 UTC |
| 9bb3a73 | Benjamin Gregoire | 15 June 2020, 13:54:10 UTC | add conseq rule : relation between choare / (bdhoare|hoare) | 15 June 2020, 13:54:10 UTC |
| e18347d | Benjamin Gregoire | 15 June 2020, 12:19:15 UTC | fix cbv with reduce logic | 15 June 2020, 12:19:15 UTC |
| ebfea0b | Benjamin Gregoire | 15 June 2020, 12:13:39 UTC | progress on example | 15 June 2020, 12:13:39 UTC |
| ca4a529 | Benjamin Gregoire | 15 June 2020, 10:43:19 UTC | small progress on complexity | 15 June 2020, 10:43:19 UTC |
| a86a8d7 | Benjamin Gregoire | 08 June 2020, 12:40:12 UTC | start complexity for hashed-elgamal | 15 June 2020, 09:23:59 UTC |
| 4ce2e4d | Adrien Koutsos | 12 June 2020, 15:54:16 UTC | Merge branch 'deploy-cost' into deploy-cost-1.0-preview | 12 June 2020, 15:54:16 UTC |
| aac1558 | Adrien Koutsos | 12 June 2020, 15:52:02 UTC | additional simplifications of cost | 12 June 2020, 15:52:02 UTC |
| 92a2cd9 | Adrien Koutsos | 12 June 2020, 15:42:40 UTC | simplification of cost judgments for datatypes and tuples. | 12 June 2020, 15:43:12 UTC |
| 3b07d18 | Pierre-Yves Strub | 02 June 2020, 14:51:17 UTC | Fix cloning of user reduction (put the correct mode) | 02 June 2020, 14:52:06 UTC |
| 88200ac | Pierre-Yves Strub | 02 June 2020, 14:51:17 UTC | Fix cloning of user reduction (put the correct mode) | 02 June 2020, 14:51:20 UTC |
| 71e0d64 | Benjamin Gregoire | 02 June 2020, 14:50:53 UTC | Merge branch 'deploy-cost' into deploy-cost-1.0-preview | 02 June 2020, 14:50:53 UTC |
| 556c55d | Benjamin Gregoire | 02 June 2020, 14:50:06 UTC | small fixes | 02 June 2020, 14:50:06 UTC |
| 32adb42 | Benjamin Gregoire | 02 June 2020, 14:17:40 UTC | Merge branch 'deploy-cost' into deploy-cost-1.0-preview | 02 June 2020, 14:17:40 UTC |
| 8133669 | Benjamin Gregoire | 02 June 2020, 14:16:53 UTC | small fixes | 02 June 2020, 14:16:53 UTC |
| 7076362 | Pierre-Yves Strub | 02 June 2020, 14:13:56 UTC | Merge branch 'deploy-cost' into deploy-cost-1.0-preview | 02 June 2020, 14:13:56 UTC |
| b9abebe | Pierre-Yves Strub | 02 June 2020, 14:13:38 UTC | cloning now supports schemas | 02 June 2020, 14:13:38 UTC |
| 794484a | Adrien Koutsos | 28 May 2020, 12:46:32 UTC | match rule for choare judgements. | 28 May 2020, 12:46:32 UTC |
| ab778a1 | Pierre-Yves Strub | 28 May 2020, 09:20:10 UTC | Merge branch 'deploy-match-in-stmt' into deploy-cost-1.0-preview | 28 May 2020, 09:20:10 UTC |
| b7af66a | Pierre-Yves Strub | 28 May 2020, 08:00:29 UTC | Merge branch '1.0' into deploy-match-in-stmt | 28 May 2020, 08:00:29 UTC |
| 8a3eafb | Pierre-Yves Strub | 28 May 2020, 07:57:19 UTC | Merge branch '1.0' into deploy-cost | 28 May 2020, 07:57:19 UTC |
| 3e8c6b5 | Benjamin Gregoire | 27 May 2020, 13:09:33 UTC | fix bug | 27 May 2020, 13:14:25 UTC |
| 6e5bd45 | Benjamin Gregoire | 27 May 2020, 13:08:56 UTC | add lemmas on bigi | 27 May 2020, 13:14:25 UTC |
| 6bc158c | Adrien Koutsos | 27 May 2020, 08:53:50 UTC | improved restr. printing | 27 May 2020, 08:53:50 UTC |
| 53ed919 | Alley Stoughton | 22 May 2020, 22:12:19 UTC | Allows nosmt with all operators other than pure, abstract ones - i.e., with plain, axiomatized (including : {t | phi} as ax) and cases operators. When cloning, [op nosmt x = ...] is allowed, but nosmt can't be used with inlining mode. | 26 May 2020, 08:38:14 UTC |
| 096de75 | Adrien Koutsos | 28 April 2020, 13:14:33 UTC | example of a section in the small tutorial. Also removed the debugging info when printing choare judgements. | 28 April 2020, 13:14:33 UTC |
| 974c7fb | Adrien Koutsos | 28 April 2020, 13:08:08 UTC | cleanup some old comments | 28 April 2020, 13:08:08 UTC |
| fe1193a | Adrien Koutsos | 28 April 2020, 13:02:37 UTC | memory printing printed in a better order. | 28 April 2020, 13:02:37 UTC |
| eee8d28 | Adrien Koutsos | 28 April 2020, 12:55:46 UTC | minor pretty printer improvements. | 28 April 2020, 12:55:46 UTC |
| be2bf40 | Adrien Koutsos | 28 April 2020, 12:55:15 UTC | import BIA for shorter paths, + minor change. | 28 April 2020, 12:55:15 UTC |
| 1311f7b | Adrien Koutsos | 28 April 2020, 12:30:38 UTC | short syntax for abs. calls with invariant when there is no oracle. | 28 April 2020, 12:30:38 UTC |
| b7463b6 | Adrien Koutsos | 28 April 2020, 12:01:53 UTC | Fixed shift/reduce conflicts | 28 April 2020, 12:01:53 UTC |
| 0ce118f | Adrien Koutsos | 28 April 2020, 11:13:08 UTC | bugs | 28 April 2020, 11:13:08 UTC |
| c55ebb4 | Adrien Koutsos | 28 April 2020, 11:05:08 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-cost | 28 April 2020, 11:05:08 UTC |
| 170c443 | Benjamin Gregoire | 27 April 2020, 12:23:05 UTC | fix default.nix | 27 April 2020, 12:23:05 UTC |
| 58aaed4 | AntoineSere | 20 April 2020, 17:02:04 UTC | Merge pull request #42 from AntoineSere/eqvquo Added two useful lemmas to Quotient.ec | 20 April 2020, 17:02:04 UTC |
| ce4d827 | Antoine Séré | 20 April 2020, 15:04:39 UTC | Added two useful lemmas to Quotient.ec | 20 April 2020, 15:04:39 UTC |
| b8e9ba6 | Adrien Koutsos | 20 April 2020, 10:49:51 UTC | renamed files | 20 April 2020, 10:49:51 UTC |
| a3cd411 | Adrien Koutsos | 16 April 2020, 15:36:20 UTC | work on FO. | 16 April 2020, 15:36:20 UTC |
| acfd4ea | Pierre-Yves Strub | 16 April 2020, 14:56:46 UTC | Definition of quotient types w.r.t. a equivalence relation | 16 April 2020, 14:56:46 UTC |
| 60a7d34 | Pierre-Yves Strub | 16 April 2020, 13:19:34 UTC | Finite groups, cyclic groups, Bezout. | 16 April 2020, 13:19:53 UTC |
| cdb2e6f | François Dupressoir | 16 April 2020, 10:45:54 UTC | Use arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '=' | 16 April 2020, 10:45:54 UTC |
| f44260c | Pierre-Yves Strub | 16 April 2020, 09:41:06 UTC | stdlib: distributions: dmap1E_can | 16 April 2020, 09:41:06 UTC |
| 94786bc | Pierre-Yves Strub | 16 April 2020, 09:40:44 UTC | stdlib: List: nth_default | 16 April 2020, 09:40:44 UTC |
| 136b237 | Pierre-Yves Strub | 15 April 2020, 09:39:30 UTC | lemma: fun_ext2 | 15 April 2020, 09:39:30 UTC |
| 5eba66b | Pierre-Yves Strub | 15 April 2020, 09:31:23 UTC | allow writing m.[i, j] in place of m.[(i, j)] | 15 April 2020, 09:31:23 UTC |
| 4882379 | Pierre-Yves Strub | 15 April 2020, 08:28:48 UTC | views: allow application of induction principle as a view | 15 April 2020, 08:28:48 UTC |
| 64d592d | Pierre-Yves Strub | 15 April 2020, 08:19:44 UTC | elim: search quantifier modulo reduction | 15 April 2020, 08:19:54 UTC |
| 3b8b038 | Adrien Koutsos | 14 April 2020, 15:08:58 UTC | Fixed unclosed box. (#41) Co-authored-by: Adrien Koutsos <akoutsos@users.noreply.github.com> | 14 April 2020, 15:08:58 UTC |
| 56b5594 | Adrien Koutsos | 14 April 2020, 14:27:28 UTC | FO | 14 April 2020, 14:28:52 UTC |
| f3581d5 | Pierre-Yves Strub | 10 April 2020, 09:56:42 UTC | binomial coefficients | 10 April 2020, 09:56:42 UTC |
| eb9b026 | Pierre-Yves Strub | 09 April 2020, 16:21:20 UTC | CI: move to slack notification | 09 April 2020, 16:22:07 UTC |
| 21e8fce | Pierre-Yves Strub | 09 April 2020, 16:21:20 UTC | CI: move to slack notification | 09 April 2020, 16:21:20 UTC |
| ffe2fd6 | Adrien Koutsos | 09 April 2020, 14:45:34 UTC | Matching issue | 09 April 2020, 14:45:34 UTC |
| d41a34d | Pierre-Yves Strub | 09 April 2020, 13:43:45 UTC | Matching for *hoareF & Pr | 09 April 2020, 13:44:05 UTC |
| 4062085 | bgregoir | 09 April 2020, 13:39:11 UTC | Merge pull request #40 from CohenCyril/nixfix default.nix: adding installFlags | 09 April 2020, 13:39:11 UTC |
| ad74e06 | Adrien Koutsos | 09 April 2020, 12:24:40 UTC | minor printing change | 09 April 2020, 12:24:40 UTC |
