| bec3930 | Pierre-Yves Strub | 27 February 2017, 12:56:22 UTC | Fix Travis syntax | 27 February 2017, 12:56:22 UTC |
| 4787ab0 | Pierre-Yves Strub | 27 February 2017, 10:44:39 UTC | Add support for travis CI. | 27 February 2017, 12:49:52 UTC |
| e055841 | Pierre-Yves Strub | 27 February 2017, 10:40:22 UTC | README | 27 February 2017, 10:40:22 UTC |
| ef13e8d | Pierre-Yves Strub | 23 February 2017, 08:43:14 UTC | FIx MANIFEST | 23 February 2017, 08:43:14 UTC |
| 2d4a41e | Pierre-Yves Strub | 21 February 2017, 22:34:38 UTC | remove emacs-based packaging script Again, docker is the way to go. | 21 February 2017, 22:34:45 UTC |
| 57ad58b | Pierre-Yves Strub | 21 February 2017, 22:30:40 UTC | removing local toolchain+PG, removing vagrant - opam is the way to go for getting EasyCrypt - EasyCrypt mode for PG has been integrated upstream - Vagrant is a nightmare (docker is the way to go) | 21 February 2017, 22:30:55 UTC |
| 263740c | François Dupressoir | 19 December 2016, 22:28:21 UTC | 'Fixing' BR93. | 19 December 2016, 22:28:21 UTC |
| 8acf8d0 | Benjamin Gregoire | 13 December 2016, 10:22:12 UTC | add ring on boolean in StdRing. | 13 December 2016, 10:22:45 UTC |
| f993902 | Pierre-Yves Strub | 10 December 2016, 09:56:56 UTC | extra corollary in bigops | 10 December 2016, 09:56:56 UTC |
| 3425756 | Pierre-Yves Strub | 15 November 2016, 20:54:16 UTC | fix conversion check of expressions (missing quantif) | 15 November 2016, 20:54:22 UTC |
| 6700014 | Pierre-Yves Strub | 28 October 2016, 15:00:56 UTC | better use deprecated functions than non existing ones | 28 October 2016, 15:01:08 UTC |
| 2c150a9 | Pierre-Yves Strub | 26 October 2016, 13:57:59 UTC | kill warnings | 26 October 2016, 13:57:59 UTC |
| eae4110 | Pierre-Yves Strub | 14 September 2016, 11:29:29 UTC | Makefile | 14 September 2016, 11:29:29 UTC |
| 495667a | Pierre-Yves Strub | 07 September 2016, 10:14:18 UTC | In `t_crush`, only substitute eqs. in variables local to the eqs. I.e., in eqs. that have been introduced after the last `split` or in all eqs. if no `split` have ocurred. [fix #17339] | 07 September 2016, 10:14:18 UTC |
| 5b35f66 | Pierre-Yves Strub | 07 September 2016, 10:13:01 UTC | t_subst: allow to do the substitution only in targeted hyps. The new parameter is `?tg` and gives the set of hypotheses identifiers in which the substitution can occur. If `tg` is `None`, the previous behaviour is applied --- i.e. try the substitution in all local hypotheses. | 07 September 2016, 10:13:01 UTC |
| c2940eb | Pierre-Yves Strub | 07 September 2016, 10:10:42 UTC | New printer for `LDecl.hyps`. | 07 September 2016, 10:10:42 UTC |
| 0c51d1f | Pierre-Yves Strub | 31 August 2016, 19:10:48 UTC | Issue a warning when an unknown `pragma` is issued. The behaviour for options (i.e. for `pragma +opt` / `pragma -opt`) is kept. [close #17338] | 31 August 2016, 19:10:48 UTC |
| 12ed9d6 | Pierre-Yves Strub | 29 August 2016, 10:58:47 UTC | Nits in `zipper_of_cpos` (catch the right exception) | 29 August 2016, 10:58:47 UTC |
| 6a1a2b5 | Pierre-Yves Strub | 29 August 2016, 10:56:37 UTC | New variant of `inline`: `inline side? codepos`. Inline the procedure call located at position `codepos`. [close #17336] | 29 August 2016, 10:56:37 UTC |
| 3d8e4b7 | Pierre-Yves Strub | 29 August 2016, 10:25:23 UTC | Add missing cases for inline (phoare / byname) | 29 August 2016, 10:25:23 UTC |
| 455162b | Pierre-Yves Strub | 27 August 2016, 07:11:21 UTC | Add a pragma for interverting `/=` && `/~=` (and all their variants) The pragma is `redlogic` (i.e. logical reduction in `/=`). It is set by default. [close #17333] | 27 August 2016, 07:12:22 UTC |
| d273f1b | Benjamin Gregoire | 24 August 2016, 16:28:20 UTC | add clone ComRing in BitWord | 24 August 2016, 16:28:20 UTC |
| 9a4f6f0 | Benjamin Gregoire | 24 August 2016, 14:58:28 UTC | add useful lemma | 24 August 2016, 14:58:28 UTC |
| 44c769a | Pierre-Yves Strub | 19 August 2016, 11:22:30 UTC | Syntax change: arguments of `exists` are now space separated [close #17331] | 19 August 2016, 11:22:30 UTC |
| 83167f7 | Pierre-Yves Strub | 19 August 2016, 10:36:02 UTC | Fix internal view's proof-term construction. [fix #17330] | 19 August 2016, 10:36:29 UTC |
| d7bb00b | François Dupressoir | 11 August 2016, 16:08:59 UTC | Morefiddling with smt. | 11 August 2016, 16:08:59 UTC |
| ee33eba | François Dupressoir | 11 August 2016, 12:39:35 UTC | smt all -> smt in AWord. | 11 August 2016, 12:39:35 UTC |
| 4f9d39d | François Dupressoir | 11 August 2016, 12:38:05 UTC | Stabilize smt in StdRing. | 11 August 2016, 12:38:05 UTC |
| 59c8860 | Pierre-Yves Strub | 11 August 2016, 01:53:00 UTC | Do not use hash-cons based ordering in places where a stable order in needed. Hash-cons based ordering is not stable from run to run. This commit adds a set a "natural" orderings for paths & related structure and use them in place where a stable ordering is needed. This might affect existing proofs that were, by chance, perfectly working. [fix #17329] | 11 August 2016, 02:10:53 UTC |
| c4a059e | Pierre-Yves Strub | 09 August 2016, 20:52:30 UTC | New variants of i.p. `<*>` The variant `<<*>` gives priority to right-to-left substitutions, whereas the variant `<*>>` gives priority to left-to-right substitutions. [closes #17327] | 09 August 2016, 20:52:30 UTC |
| 8feea6f | Pierre-Yves Strub | 09 August 2016, 11:11:08 UTC | i-p `+` do not reorder goals anymore when separated by non-intro i-p. [fix #17326] | 09 August 2016, 11:11:08 UTC |
| 80d3044 | Pierre-Yves Strub | 08 August 2016, 13:54:01 UTC | i-p |> do not unfold anymore conclusion when applying `split` [fix #17324] | 08 August 2016, 13:54:10 UTC |
| a885d8c | Pierre-Yves Strub | 07 August 2016, 21:16:03 UTC | In `crush`: do not clear substituted variables. They may still be needed by the upper layer. [fix #17323] | 07 August 2016, 21:16:03 UTC |
| b0f6ae6 | Pierre-Yves Strub | 06 August 2016, 15:21:27 UTC | In subst: add support for inductive predicates. [fix #17320] | 06 August 2016, 15:21:27 UTC |
| b2d38f8 | Pierre-Yves Strub | 06 August 2016, 14:10:22 UTC | In parser: `case` options are not before the colon, not after [fix #17321] | 06 August 2016, 14:10:28 UTC |
| 30570db | Pierre-Yves Strub | 06 August 2016, 14:05:43 UTC | In parser, do not shuffle proofs/renaming of a clone [fix #17318] | 06 August 2016, 14:05:49 UTC |
| ac945f3 | Pierre-Yves Strub | 06 August 2016, 14:05:01 UTC | fix scripts w.r.t new auto DB | 06 August 2016, 14:05:01 UTC |
| f6b75ac | Pierre-Yves Strub | 15 July 2016, 15:55:21 UTC | push missing files | 15 July 2016, 15:55:21 UTC |
| 1188240 | Benjamin Gregoire | 15 July 2016, 15:19:25 UTC | fix simplification of know real expression. | 15 July 2016, 15:19:37 UTC |
| 8a723c3 | Pierre-Yves Strub | 15 July 2016, 15:04:26 UTC | fix namings | 15 July 2016, 15:04:37 UTC |
| 293e676 | Pierre-Yves Strub | 15 July 2016, 15:00:52 UTC | some facts on ln | 15 July 2016, 15:01:01 UTC |
| 920939f | Pierre-Yves Strub | 15 July 2016, 14:50:24 UTC | analysis: some facts on convexity | 15 July 2016, 14:50:24 UTC |
| fd59217 | Pierre-Yves Strub | 15 July 2016, 10:28:16 UTC | axiomatized bounds for ln | 15 July 2016, 10:28:29 UTC |
| 2e8bc62 | Pierre-Yves Strub | 15 July 2016, 10:11:10 UTC | add real square root | 15 July 2016, 10:11:10 UTC |
| 9a21032 | Pierre-Yves Strub | 15 July 2016, 08:23:33 UTC | async while: fix bugs regarding fresh variables | 15 July 2016, 08:26:46 UTC |
| 4bc331a | Pierre-Yves Strub | 15 July 2016, 07:34:43 UTC | tremendeous hacks for fixing subst. of locals | 15 July 2016, 08:26:39 UTC |
| f7b4f66 | Benjamin Gregoire | 14 July 2016, 20:50:14 UTC | improve usability of async while. | 15 July 2016, 08:26:01 UTC |
| c17c154 | Pierre-Yves Strub | 14 July 2016, 14:20:31 UTC | async-while prototype implementation (to be tested) | 14 July 2016, 14:20:31 UTC |
| 234f832 | Pierre-Yves Strub | 14 July 2016, 09:28:15 UTC | do not use Map.translate on non monotonous funs | 14 July 2016, 09:30:27 UTC |
| 22d52f3 | Pierre-Yves Strub | 07 July 2016, 10:26:54 UTC | Work around #17319 [references #17319] | 07 July 2016, 10:26:54 UTC |
| ec6fca2 | Pierre-Yves Strub | 13 June 2016, 15:36:23 UTC | fix compilation on ocaml 4.03.0 | 13 June 2016, 15:36:32 UTC |
| 377a2cd | François Dupressoir | 31 May 2016, 13:25:57 UTC | NewFMap: avoid using finite sets when predicates work (eq_except). | 31 May 2016, 13:25:57 UTC |
| 3c30914 | François Dupressoir | 31 May 2016, 11:56:23 UTC | Stablizing an smt call in NewFMap. | 31 May 2016, 11:56:23 UTC |
| c9a0683 | François Dupressoir | 19 May 2016, 10:03:13 UTC | Everything (in theories) is NewFMap. | 19 May 2016, 10:03:39 UTC |
| f9d70ed | Pierre-Yves Strub | 18 May 2016, 16:09:18 UTC | balancing .dir-locals | 18 May 2016, 16:09:18 UTC |
| 4be663f | Pierre-Yves Strub | 17 May 2016, 16:00:05 UTC | README.md | 17 May 2016, 16:00:05 UTC |
| fd4bf22 | Pierre-Yves Strub | 07 May 2016, 09:41:02 UTC | Nits. | 07 May 2016, 09:41:02 UTC |
| fcf86c2 | Pierre-Yves Strub | 06 May 2016, 19:59:40 UTC | List masking. | 06 May 2016, 19:59:40 UTC |
| 407be6f | Pierre-Yves Strub | 06 May 2016, 14:34:18 UTC | Killing a bunch of admits in intdiv + defining ediv. | 06 May 2016, 14:34:18 UTC |
| 3dedf33 | Pierre-Yves Strub | 06 May 2016, 09:43:25 UTC | Don't use the currently printed abbrev. when printing its body. [fix #17135] | 06 May 2016, 09:44:11 UTC |
| c8fbd0c | François Dupressoir | 06 May 2016, 08:49:44 UTC | Argmin is now a real argmin. | 06 May 2016, 08:49:44 UTC |
| ff23f9a | François Dupressoir | 06 May 2016, 08:39:52 UTC | argmin: remove existentials in premises. | 06 May 2016, 08:39:52 UTC |
| 22578b4 | Pierre-Yves Strub | 06 May 2016, 07:38:09 UTC | `argmin` operator `argmin p` returns the smaller natural `i` s.t. `p i` or 0 if not such witness exists. | 06 May 2016, 07:38:09 UTC |
| fa61550 | Pierre-Yves Strub | 05 May 2016, 19:31:40 UTC | Add negative filters for `clone ... proof * [...]` Filters now have the following syntax: `[-?tag ... -?tag]` Negative tags are of the form `-tag`. Other ones are named positive. An axiom is selected by a filter if: - none of its tags are rejected by a negative filters - one of its tags is accepted by a positive filter or no positive filters exists | 05 May 2016, 19:31:40 UTC |
| 6c9dfe5 | Pierre-Yves Strub | 05 May 2016, 09:28:49 UTC | Properly equip zmod with a ring structure. The inverse is currently not linked to gcd. | 05 May 2016, 09:29:36 UTC |
| bf94ca4 | François Dupressoir | 04 May 2016, 11:21:37 UTC | Moving Word away from Arrays. Updating MEE functional spec accordingly. | 04 May 2016, 11:21:45 UTC |
| 0670411 | François Dupressoir | 04 May 2016, 11:19:46 UTC | Stabilize smt in MEE instantiation. | 04 May 2016, 11:19:46 UTC |
| ccd68ba | Pierre-Yves Strub | 30 April 2016, 13:47:02 UTC | In `clone`: when renaming, don't forget to prepend sub-theorie path as a prefix. [fix #17312] | 30 April 2016, 13:47:02 UTC |
| aa6ee8e | Pierre-Yves Strub | 30 April 2016, 11:30:50 UTC | Homogenise module & module type parameters syntax. [fix #17314] | 30 April 2016, 11:30:50 UTC |
| 6bd35fb | Pierre-Yves Strub | 30 April 2016, 10:53:33 UTC | In mod-typing: clean-up dead code, remove internal exn., fix various bugs. [fix #17313] | 30 April 2016, 10:53:33 UTC |
| dff9911 | Pierre-Yves Strub | 29 April 2016, 19:32:49 UTC | bigop: partition | 29 April 2016, 19:33:12 UTC |
| 0014c65 | François Dupressoir | 27 April 2016, 13:20:53 UTC | Using (semi-)modern libs for MEE-CBC functional spec. Some discussion need to be had: - Should we bring everything back to bitstrings? octetstrings? - Should we get rid of those blasted Arrays? (Yes) | 27 April 2016, 15:06:22 UTC |
| 8db4a56 | François Dupressoir | 25 April 2016, 16:55:16 UTC | Stabilizing some smt calls and fixing a proof. | 25 April 2016, 16:55:16 UTC |
| 4702c81 | François Dupressoir | 22 April 2016, 17:58:46 UTC | More systematic construction for the partitioning of final states. | 22 April 2016, 17:58:46 UTC |
| 4bfe658 | François Dupressoir | 22 April 2016, 15:15:56 UTC | Starting cleanup in Dice_sampling and associated example. | 22 April 2016, 15:15:56 UTC |
| 179af54 | François Dupressoir | 22 April 2016, 14:34:11 UTC | Preliminary generic argument for event partitioning. This kind of argument is currently difficult to use, but formalizing and using them should give us hints as to what we can and should do to support them more cleanly. This one will be used, once generalized further and cleaned up, to simplify Dice_sampling. | 22 April 2016, 14:44:11 UTC |
| db89cbe | François Dupressoir | 22 April 2016, 13:18:48 UTC | Generalizing dscale into DScalar with backwards comp. | 22 April 2016, 14:44:11 UTC |
| 85d276d | Pierre-Yves Strub | 19 April 2016, 21:00:33 UTC | do generalization modulo alpha-eq, not conv | 19 April 2016, 21:00:42 UTC |
| ac9b6e7 | François Dupressoir | 07 April 2016, 16:14:04 UTC | Cleaning up and 'documenting' Benjamin's general Eager argument. | 07 April 2016, 16:14:04 UTC |
| 7fe5299 | François Dupressoir | 07 April 2016, 15:41:06 UTC | Very minor on NewFMap. | 07 April 2016, 15:41:06 UTC |
| 2318135 | François Dupressoir | 05 April 2016, 16:49:49 UTC | Expanding set of operators on relations. | 05 April 2016, 16:49:49 UTC |
| 5e9884e | François Dupressoir | 05 April 2016, 14:28:07 UTC | PRG example: some major changes. Switch to using explicit distributions and probability; Switch to preferred proof engine setup (newip, implicits); Switch to inductives for bad event and invariant; More stability fixes. | 05 April 2016, 14:28:07 UTC |
| 77d2c90 | François Dupressoir | 05 April 2016, 12:29:33 UTC | PG keywords | 05 April 2016, 12:29:38 UTC |
| 6e1520f | François Dupressoir | 05 April 2016, 08:16:28 UTC | Minor cleanup in PRG. | 05 April 2016, 08:16:28 UTC |
| 0778000 | François Dupressoir | 28 March 2016, 16:51:55 UTC | MEE-CBC: cleanup and smt stabilization (in CBC). | 04 April 2016, 08:58:29 UTC |
| c770168 | Pierre-Yves Strub | 02 April 2016, 08:12:48 UTC | build-linux: do not force toolchain version anymore | 02 April 2016, 08:12:48 UTC |
| ce05896 | Pierre-Yves Strub | 02 April 2016, 08:11:52 UTC | README: add ZArith in deps. | 02 April 2016, 08:11:52 UTC |
| 8204617 | Pierre-Yves Strub | 02 April 2016, 08:09:32 UTC | Why3: => 0.87 | 02 April 2016, 08:09:32 UTC |
| 9d80a0e | Pierre-Yves Strub | 28 March 2016, 19:24:26 UTC | fix packaging for linux-32 | 28 March 2016, 19:24:47 UTC |
| 250b54f | François Dupressoir | 28 March 2016, 13:19:31 UTC | MEE-CBC: making further use of new standard libraries. | 28 March 2016, 13:19:43 UTC |
| d597a68 | Pierre-Yves Strub | 25 March 2016, 07:43:56 UTC | Update README.md | 25 March 2016, 07:43:56 UTC |
| d1bbeb2 | Pierre-Yves Strub | 16 March 2016, 20:20:10 UTC | linux packaging: fix PG conf | 16 March 2016, 20:20:20 UTC |
| 9330f1e | Pierre-Yves Strub | 11 March 2016, 14:49:04 UTC | dbhints can now be empty. For example, `smt()` is `smt w=()` which implies `smt ml=0`. | 11 March 2016, 14:49:04 UTC |
| 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 |
