| 85cdb3f | Pierre-Yves Strub | 10 March 2016, 21:52:44 UTC | smt(...) is now an alias for smt w=(...) | 10 March 2016, 21:52:44 UTC |
| 34aab04 | François Dupressoir | 10 March 2016, 10:30:11 UTC | Updating a few examples. | 10 March 2016, 10:30:11 UTC |
| 9df4dd0 | François Dupressoir | 10 March 2016, 10:13:28 UTC | Removing obsolete PRP-PRF example. An up-to-date and maintained version can be found in theories/crypto/prp_prf/RP_RF.eca | 10 March 2016, 10:13:33 UTC |
| 12a4465 | François Dupressoir | 09 March 2016, 15:54:32 UTC | Quick and Dirty fix for Hashed ElGamal. | 09 March 2016, 15:54:32 UTC |
| e365fbf | François Dupressoir | 07 March 2016, 13:48:39 UTC | PRG example: some update and stabilization. | 07 March 2016, 13:48:39 UTC |
| 123baa8 | Pierre-Yves Strub | 05 March 2016, 16:18:17 UTC | Distribute ecVersion.ml.in, not ecVersion.ml | 05 March 2016, 16:18:17 UTC |
| 1b99c89 | Pierre-Yves Strub | 04 March 2016, 19:14:32 UTC | easycrypt config now displays the git hash | 04 March 2016, 19:15:00 UTC |
| b31f19f | Pierre-Yves Strub | 04 March 2016, 15:07:52 UTC | remove stalled examples (now in stdlib) | 04 March 2016, 15:07:52 UTC |
| cc6f725 | Pierre-Yves Strub | 26 February 2016, 16:03:19 UTC | Bind local modules when pretty-printing quantifiers [fix #17304] | 26 February 2016, 16:03:19 UTC |
| 535a27e | Pierre-Yves Strub | 26 February 2016, 11:38:40 UTC | exclude `oldlibs` from tests | 26 February 2016, 11:38:47 UTC |
| 29d815d | François Dupressoir | 26 February 2016, 11:36:38 UTC | Stabilize smt call in LazyEager | 26 February 2016, 11:36:38 UTC |
| 83edf64 | François Dupressoir | 26 February 2016, 11:32:29 UTC | Fixing RP_RF after Benjamin's changes to Birthday. Further extending Birthday to allow 0 queries. | 26 February 2016, 11:32:29 UTC |
| 87b373a | Benjamin Gregoire | 25 February 2016, 15:29:40 UTC | simplify the proof using advantage of the new fel. | 25 February 2016, 15:29:40 UTC |
| 5a66208 | Benjamin Gregoire | 25 February 2016, 12:32:12 UTC | Improve conditions for fel tactics. fix the corresponding proof. | 25 February 2016, 12:32:12 UTC |
| 33cc6c2 | Benjamin Gregoire | 25 February 2016, 10:00:54 UTC | fix commit fe97e0e2ebbb35a7fcdc77b022b19cadac8f7cf5. remove eprintf | 25 February 2016, 10:00:54 UTC |
| 784ba2c | Benjamin Gregoire | 25 February 2016, 09:19:01 UTC | [fix #17303] [fix #16416] fix bug in fel. | 25 February 2016, 09:19:01 UTC |
| 532c138 | Benjamin Gregoire | 25 February 2016, 06:04:17 UTC | Fix #17302. | 25 February 2016, 06:04:17 UTC |
| fe97e0e | Benjamin Gregoire | 24 February 2016, 17:33:43 UTC | bind NewMap with smt. Should be improved | 24 February 2016, 17:33:56 UTC |
| 20ebcf5 | Benjamin Gregoire | 24 February 2016, 15:20:43 UTC | add the constant function in NewMap | 24 February 2016, 17:33:56 UTC |
| ac1e46b | Pierre-Yves Strub | 24 February 2016, 15:25:01 UTC | Stdlib: sumidE (for reals). | 24 February 2016, 15:25:08 UTC |
| e35704b | Benjamin Gregoire | 24 February 2016, 15:05:11 UTC | Fix NewMap theory. Should make the link with smt. | 24 February 2016, 15:05:11 UTC |
| 4028dec | Benjamin Gregoire | 24 February 2016, 14:46:37 UTC | Fix smt call in Real.ec | 24 February 2016, 14:46:37 UTC |
| 0f9e6ab | Benjamin Gregoire | 24 February 2016, 13:11:16 UTC | Fix theories. | 24 February 2016, 13:12:12 UTC |
| dac6d8a | Benjamin Gregoire | 24 February 2016, 13:10:35 UTC | Fix bound in Fel. | 24 February 2016, 13:12:12 UTC |
| 590cf44 | Pierre-Yves Strub | 24 February 2016, 10:13:44 UTC | Revert "FEL: fix bug related to the move from felsum to bigi" This reverts commit 6162a495cfddd16a77873d3b63f82fb7040b9c62. | 24 February 2016, 10:13:44 UTC |
| 16a7d54 | Pierre-Yves Strub | 24 February 2016, 10:13:32 UTC | Revert "Fix stdlib w.r.t new FEL" This reverts commit 24a050a0586a0ccd9c9a04e49ee2904425861c85. | 24 February 2016, 10:13:32 UTC |
| 24a050a | Pierre-Yves Strub | 24 February 2016, 09:18:25 UTC | Fix stdlib w.r.t new FEL | 24 February 2016, 09:18:25 UTC |
| 6162a49 | Pierre-Yves Strub | 24 February 2016, 09:14:07 UTC | FEL: fix bug related to the move from felsum to bigi | 24 February 2016, 09:14:07 UTC |
| 11eccbe | Pierre-Yves Strub | 23 February 2016, 09:49:06 UTC | Abstract PCRE in the EcRegexp module | 23 February 2016, 09:50:36 UTC |
| ba9bd74 | Benjamin Gregoire | 22 February 2016, 08:34:13 UTC | improve error messages | 22 February 2016, 08:34:13 UTC |
| d9dbd96 | Benjamin Gregoire | 20 February 2016, 06:42:31 UTC | fix theories for the new module syntax | 20 February 2016, 06:42:31 UTC |
| 806353c | Benjamin Gregoire | 19 February 2016, 18:37:14 UTC | Improve typing of module and modify the syntax for declaration: module type T = { proc f() : unit }. module A (T : T) = {}. module type S0 = {}. module type S = { proc f() : unit }. module type C(X : S0) = { proc f() : unit }. module type C1(X : S) = { proc f() : unit }. module type C2(X1:S, X2:S0) = { proc f() : unit }. (* D takes an S, not just an S0 but D isn't a C, in the sense that it needs not just an S0 but an actual S to provide f() : unit *) module D (X : S) : T = { proc f() : unit = { X.f(); } }. module (D1:C1) (X : S) : T = { proc f() : unit = { X.f(); } }. (* (* This one raise an error *) module (D1':C) (X : S) : T = { proc f() : unit = { X.f(); } }. this module does not meet its interface: for argument X: S0 is not a subtype of S because procedure `f' is missing *) (* (* This one raise an error *) module (D4:C2)(X : S) = { proc f() : unit = { X.f(); } }. this module does not meet its interface: not the same number of module arguments *) (* (* This one raise an error *) module D3 (X : S) : C1 = { proc f() : unit = { X.f(); } }. this module does not meet its interface: not the same number of module arguments *) module (D2 : C,C1) (X : S0) = { proc f() : unit = { } }. | 19 February 2016, 18:37:14 UTC |
| 37ac8d8 | Pierre-Yves Strub | 18 February 2016, 08:18:40 UTC | `congr` now handles `if ... then ... else ...`. | 18 February 2016, 08:18:40 UTC |
| 6dc4662 | Pierre-Yves Strub | 17 February 2016, 19:43:18 UTC | In `apply`, try `iffRL` view before `iffLR`. | 17 February 2016, 19:43:18 UTC |
| ba7b059 | Pierre-Yves Strub | 17 February 2016, 17:39:04 UTC | fix bug in clear intro-pattern (was using H internally) | 17 February 2016, 17:39:04 UTC |
| f4c24e2 | Pierre-Yves Strub | 17 February 2016, 15:41:00 UTC | make use of new parsing rules for %r | 17 February 2016, 15:41:00 UTC |
| 78a448c | Pierre-Yves Strub | 17 February 2016, 15:40:12 UTC | fix parsing/printing of %r | 17 February 2016, 15:40:19 UTC |
| b80a21e | Benjamin Gregoire | 17 February 2016, 15:39:24 UTC | add missing trivial lemmas | 17 February 2016, 15:39:43 UTC |
| c468532 | Pierre-Yves Strub | 16 February 2016, 14:14:28 UTC | Change `rewrite` behaviour w.r.t. boolean rewriting. `rewrite` now tries to rewrite the equation `e = true` where `e` is the rewrite term before `rewrite` does its first operator unfolding. | 16 February 2016, 14:14:28 UTC |
| c3588f2 | Pierre-Yves Strub | 16 February 2016, 14:13:18 UTC | Tweaking vagrant GUI box. | 16 February 2016, 14:13:18 UTC |
| 19abbdd | Pierre-Yves Strub | 11 February 2016, 13:07:07 UTC | vagrant (GUI version) | 11 February 2016, 13:07:07 UTC |
| 09966ad | Pierre-Yves Strub | 10 February 2016, 07:46:11 UTC | removing old & unused Dmulti lib. | 10 February 2016, 07:46:11 UTC |
| a00a536 | François Dupressoir | 04 February 2016, 22:38:20 UTC | Random permutation some proofs. | 04 February 2016, 22:38:20 UTC |
| a858224 | François Dupressoir | 03 February 2016, 18:33:40 UTC | Strong PRP-PRF switching lemma works for 0 queries. | 03 February 2016, 18:33:40 UTC |
| e025b20 | François Dupressoir | 03 February 2016, 17:37:45 UTC | Adding library lemmas. | 03 February 2016, 17:38:07 UTC |
| d99c749 | Pierre-Yves Strub | 03 February 2016, 05:31:56 UTC | Fix casing of some filenames | 03 February 2016, 05:31:56 UTC |
| 3b2ac49 | Pierre-Yves Strub | 03 February 2016, 05:29:59 UTC | .gitignore: *smt, *.why (at root) | 03 February 2016, 05:29:59 UTC |
| 0be3935 | Pierre-Yves Strub | 03 February 2016, 05:28:47 UTC | Add missing copyright headers. | 03 February 2016, 05:28:47 UTC |
| 3f4f1e2 | Pierre-Yves Strub | 03 February 2016, 05:27:17 UTC | Add ProofGeneral mode in the auto-license targer. | 03 February 2016, 05:27:53 UTC |
| 2cbc445 | Pierre-Yves Strub | 03 February 2016, 05:27:06 UTC | Add a copyright to ProofGeneral mode. | 03 February 2016, 05:27:52 UTC |
| 96d7862 | Pierre-Yves Strub | 03 February 2016, 05:26:48 UTC | licensing script: support for elisp-style comments | 03 February 2016, 05:26:48 UTC |
| a47cd02 | Pierre-Yves Strub | 02 February 2016, 14:22:30 UTC | kill all axioms of Number | 02 February 2016, 14:22:30 UTC |
| 9331c08 | Pierre-Yves Strub | 02 February 2016, 13:32:40 UTC | killing some admits in NewDistr | 02 February 2016, 13:32:40 UTC |
| a6b0c38 | Pierre-Yves Strub | 02 February 2016, 13:23:39 UTC | Fixing admits in uniform distributions | 02 February 2016, 13:23:39 UTC |
| 20599b8 | Pierre-Yves Strub | 02 February 2016, 13:18:44 UTC | fix. mrat_eqP statement and prove it | 02 February 2016, 13:21:05 UTC |
| 71b03bd | François Dupressoir | 02 February 2016, 10:49:47 UTC | NewDistr: fixing drat spec. Also marking one place where a lemma from Distr is used and needs to be ported over. | 02 February 2016, 10:49:47 UTC |
| e71af98 | François Dupressoir | 02 February 2016, 10:04:35 UTC | NewDistr: taking over dmap/dapply from Distr. | 02 February 2016, 10:05:00 UTC |
| e3bed45 | François Dupressoir | 02 February 2016, 09:59:46 UTC | RealSeries: sum0 | 02 February 2016, 09:59:46 UTC |
| f8394a1 | Pierre-Yves Strub | 31 January 2016, 19:47:20 UTC | Vagrant: define 2 machines - easycrypt: shared folder, not X11, public base box - easycrypt-gui: cloned easycrypt, X11 (unity), home-made base box | 31 January 2016, 19:47:20 UTC |
| 74d19dd | Pierre-Yves Strub | 29 January 2016, 09:20:18 UTC | make von Neumann an abstract theory | 29 January 2016, 13:27:23 UTC |
| 09e92e3 | Pierre-Yves Strub | 29 January 2016, 07:40:57 UTC | Simplifying von Neumann example. | 29 January 2016, 13:27:23 UTC |
| acd25c7 | François Dupressoir | 28 January 2016, 10:40:01 UTC | Filling in an admit. This is to get familiar with summability. The proof needs looked at. | 28 January 2016, 10:40:01 UTC |
| f21ba4c | Pierre-Yves Strub | 27 January 2016, 16:17:20 UTC | internal API change for checking formula in *hl goals | 27 January 2016, 16:17:27 UTC |
| e379fcf | François Dupressoir | 27 January 2016, 09:41:04 UTC | Modernizing dinter and updating stdlib. | 27 January 2016, 09:41:04 UTC |
| 729da1a | Pierre-Yves Strub | 27 January 2016, 00:16:58 UTC | Cleaning a bit br93. (nothing deep) | 27 January 2016, 00:16:58 UTC |
| 60dffa8 | Pierre-Yves Strub | 27 January 2016, 00:10:32 UTC | BR93 is back- but still ugly. | 27 January 2016, 00:10:39 UTC |
| 4cafb1e | François Dupressoir | 26 January 2016, 18:48:48 UTC | One more example re-established. | 26 January 2016, 18:48:48 UTC |
| f4d55f0 | François Dupressoir | 26 January 2016, 18:43:59 UTC | Nits in DProd. | 26 January 2016, 18:43:59 UTC |
| b639c79 | François Dupressoir | 26 January 2016, 16:42:20 UTC | Minor cleanup in DList. | 26 January 2016, 16:42:20 UTC |
| 69e4fff | François Dupressoir | 26 January 2016, 16:41:20 UTC | Dropping DEmpty and DUnit. Use dnull and MUnit.dunit from NewDistr instead. | 26 January 2016, 16:41:20 UTC |
| bb6e7f1 | François Dupressoir | 26 January 2016, 16:27:38 UTC | Fixing examples that currently work w.r.t. new product distribution. | 26 January 2016, 16:27:38 UTC |
| c5c4f43 | François Dupressoir | 26 January 2016, 16:27:18 UTC | Switching to NewDistr for product distributions. | 26 January 2016, 16:27:18 UTC |
| 046650e | François Dupressoir | 26 January 2016, 15:59:57 UTC | Sampling in DProd and sampling both components are equivalent. | 26 January 2016, 15:59:57 UTC |
| 12bcb32 | François Dupressoir | 26 January 2016, 11:51:23 UTC | Maintaining examples that currently go through. | 26 January 2016, 11:51:23 UTC |
| ab26ad8 | François Dupressoir | 26 January 2016, 11:50:52 UTC | Distribution-filtering is now predicate-based. Fixing stdlib for this and other commits. | 26 January 2016, 11:50:52 UTC |
| ec15d84 | Pierre-Yves Strub | 25 January 2016, 21:48:31 UTC | At the end of `crush`, don't use delta when simplify. | 25 January 2016, 21:48:50 UTC |
| 93cd53b | François Dupressoir | 25 January 2016, 21:06:21 UTC | Updating vonNeumann to use new Dexcepted. Issues introduced by an earlier commit on `crush` are also fixed here. | 25 January 2016, 21:06:34 UTC |
| 666c7c6 | François Dupressoir | 25 January 2016, 21:04:56 UTC | Modernizing Drestrict and Dexcepted. Updating standard lib. We still need to make sure that Distr.Drestr and Distr.Dexcepted are not used anywhere else. Then burn them down and dance on their ashes. | 25 January 2016, 21:04:56 UTC |
| 11d8d1b | François Dupressoir | 25 January 2016, 16:53:36 UTC | NewDistr product distribution: a first stab. Holes to be filled in regarding sums over lists of pairs. A note worthy of discussion and changes if one thinks them necessary. And somthing to do before the old Pair.Dprod can be swapped out entirely. | 25 January 2016, 16:53:36 UTC |
| c0b807b | Pierre-Yves Strub | 25 January 2016, 11:57:21 UTC | `crush` now ends with a goal simplification. | 25 January 2016, 11:57:21 UTC |
| 682eacf | Pierre-Yves Strub | 25 January 2016, 11:51:21 UTC | In `|>` & `/>`, only rewrite hypotheses using alpha-conv. | 25 January 2016, 11:51:21 UTC |
| 22824dd | Pierre-Yves Strub | 25 January 2016, 11:39:53 UTC | Enhance hyps. conversion. | 25 January 2016, 11:39:53 UTC |
| 22e81c4 | Pierre-Yves Strub | 25 January 2016, 10:31:10 UTC | New distr: biased coins. | 25 January 2016, 10:31:10 UTC |
| b7be81c | Pierre-Yves Strub | 23 January 2016, 20:59:25 UTC | Fix MEE-CBC (weak-check) | 23 January 2016, 20:59:25 UTC |
| 33fe060 | Pierre-Yves Strub | 23 January 2016, 20:59:05 UTC | Add a test-config entry for MEE-CBC. | 23 January 2016, 20:59:05 UTC |
| 8430fab | François Dupressoir | 23 January 2016, 12:45:13 UTC | Aftermath of fixes in Number. | 23 January 2016, 12:45:13 UTC |
| 06952da | François Dupressoir | 23 January 2016, 11:49:25 UTC | Fix the Numbers fix. | 23 January 2016, 11:49:25 UTC |
| 8dd0763 | Pierre-Yves Strub | 22 January 2016, 20:20:38 UTC | some fix in Numbers | 22 January 2016, 20:20:38 UTC |
| a9eab14 | Pierre-Yves Strub | 22 January 2016, 14:19:14 UTC | module namespace can now be prefixed by Top/Self. [fix #17294] | 22 January 2016, 14:19:14 UTC |
| 9a70f94 | Pierre-Yves Strub | 22 January 2016, 13:51:31 UTC | Tweaking reals simplification | 22 January 2016, 13:51:31 UTC |
| dcb60df | Pierre-Yves Strub | 22 January 2016, 11:40:00 UTC | Fix various bugs in real simplification. [fix #17293] | 22 January 2016, 11:40:27 UTC |
| c96ffdb | François Dupressoir | 22 January 2016, 11:38:41 UTC | A quick cleanup of one example. Highlights some missing things in real summability. | 22 January 2016, 11:38:41 UTC |
| 9633859 | François Dupressoir | 22 January 2016, 10:18:36 UTC | Adding lemmas on injectivity of rcons. | 22 January 2016, 10:18:36 UTC |
| 5dac0f2 | François Dupressoir | 22 January 2016, 10:17:38 UTC | Adding some support lemmas to NewLogic. Plus some cleanup. | 22 January 2016, 10:17:38 UTC |
| dda4828 | Pierre-Yves Strub | 21 January 2016, 17:43:53 UTC | `progress*`-like intro-pattern. `move=> |>` does a `progress` like job, but merges all the generated subgoals as their conjunction. `move=> />` does the same, but up to delta-conversion. | 21 January 2016, 17:43:53 UTC |
| 30dfd89 | Pierre-Yves Strub | 21 January 2016, 14:17:17 UTC | Fixing stdlib w.r.t recent changes | 21 January 2016, 14:17:53 UTC |
| a2baa23 | Pierre-Yves Strub | 21 January 2016, 14:04:41 UTC | New intro-pattern: + `move=> n?` is equivalent to `move=> ?` n times + `move=> *` is equivalent to `move=> ?` as much as possible. | 21 January 2016, 14:17:53 UTC |
| 4114134 | Pierre-Yves Strub | 21 January 2016, 11:37:59 UTC | Allow i-p: `n!->>` & syntax change for `n!->`. | 21 January 2016, 14:17:53 UTC |
| f4831e6 | Pierre-Yves Strub | 21 January 2016, 11:07:03 UTC | In newip, change name generation of anonymous variables. | 21 January 2016, 14:05:29 UTC |
| 9053345 | Pierre-Yves Strub | 21 January 2016, 09:54:48 UTC | Tacticals now support to be decorated with intro-patterns. | 21 January 2016, 14:05:29 UTC |
