b1c2c84 | Pierre-Yves Strub | 04 July 2014, 10:48:55 UTC | Tuples equality simplification now uses symmetric equality. | 04 July 2014, 10:48:55 UTC |
7f70b66 | Pierre-Yves Strub | 04 July 2014, 10:25:58 UTC | Reduction of equality between concrete tuples. | 04 July 2014, 10:25:58 UTC |
dee4e63 | Pierre-Yves Strub | 02 July 2014, 10:17:35 UTC | Dead code removal | 02 July 2014, 10:17:35 UTC |
72b59f2 | Pierre-Yves Strub | 01 July 2014, 20:56:46 UTC | [make toolchain] now works under cygwin (32) | 01 July 2014, 20:58:04 UTC |
1764a53 | Pierre-Yves Strub | 01 July 2014, 19:35:13 UTC | Test for forward apply in intros. | 01 July 2014, 19:35:13 UTC |
f0f2a2b | Pierre-Yves Strub | 01 July 2014, 19:28:58 UTC | Forward apply in intro pattern. Syntax: move=> /pf. | 01 July 2014, 19:28:58 UTC |
08b8ffe | Francois Dupressoir | 01 July 2014, 12:56:04 UTC | Marking a controversial lemma as nosmt. | 01 July 2014, 12:56:04 UTC |
cf12dc4 | Pierre-Yves Strub | 26 June 2014, 19:35:04 UTC | Test for intro-pattern <<- & ->>. | 26 June 2014, 19:35:04 UTC |
2b63167 | Pierre-Yves Strub | 26 June 2014, 19:29:53 UTC | New intro-pattern: <<- && ->> Introduce the hypothesis, which is expected to be an equality between a variable and a term, and do the substitution of the variable. [->>] (resp [<<-]) expects the variable to be on the left (resp. right). | 26 June 2014, 19:29:53 UTC |
3fbffa7 | Pierre-Yves Strub | 26 June 2014, 18:40:21 UTC | Add new arrows: <<- && ->> | 26 June 2014, 18:40:21 UTC |
7b3b04d | Pierre-Yves Strub | 26 June 2014, 10:05:03 UTC | Add an elimintation principle of the unit type. | 26 June 2014, 10:05:03 UTC |
35d7517 | Pierre-Yves Strub | 26 June 2014, 09:55:49 UTC | Search for the elimintation principle using the head-normal form of a type. | 26 June 2014, 09:55:49 UTC |
9f3d473 | Pierre-Yves Strub | 26 June 2014, 09:16:06 UTC | Negative occurences selection. | 26 June 2014, 09:16:06 UTC |
f12cf14 | Pierre-Yves Strub | 26 June 2014, 09:11:27 UTC | Don't crash when using [proof] outside of a proof. | 26 June 2014, 09:11:27 UTC |
667ec96 | Pierre-Yves Strub | 25 June 2014, 17:12:50 UTC | Fix notification w.r.t. lemmas / axioms. | 25 June 2014, 17:13:07 UTC |
3487b1d | Francois Dupressoir | 24 June 2014, 16:29:09 UTC | Adding rng operator. | 24 June 2014, 16:29:09 UTC |
266d5c9 | Benjamin Gregoire | 23 June 2014, 14:28:40 UTC | Add trivial module in Pair | 23 June 2014, 14:28:50 UTC |
ea70757 | Benjamin Gregoire | 23 June 2014, 14:27:55 UTC | Fixing part of the bug 17029. | 23 June 2014, 14:28:50 UTC |
2aaca80 | Pierre-Yves Strub | 22 June 2014, 23:05:51 UTC | Pattern matching now supports meta-var for memories. | 22 June 2014, 23:05:51 UTC |
fdc7039 | Pierre-Yves Strub | 22 June 2014, 22:08:39 UTC | Update copyright for command line interface. | 22 June 2014, 22:08:39 UTC |
3c18074 | Pierre-Yves Strub | 22 June 2014, 22:02:17 UTC | Update copyright on all source files. | 22 June 2014, 22:02:17 UTC |
35acf25 | Pierre-Yves Strub | 22 June 2014, 22:01:13 UTC | Script for setting / updating copyright on source files. | 22 June 2014, 22:01:13 UTC |
bb4b80a | Francois Dupressoir | 20 June 2014, 09:54:19 UTC | Updating keywords. | 20 June 2014, 09:54:19 UTC |
997d5d4 | Benjamin Gregoire | 19 June 2014, 07:49:50 UTC | Fix theory IRing | 19 June 2014, 07:49:50 UTC |
8bc5765 | Benjamin Gregoire | 19 June 2014, 07:49:32 UTC | Fixing bug #17027 and #17028 | 19 June 2014, 07:49:32 UTC |
6a7878b | Francois Dupressoir | 18 June 2014, 14:41:26 UTC | Fixing ROM and test after bugfix. The old test should be used as negative test. | 18 June 2014, 14:41:26 UTC |
138c4ab | Pierre-Yves Strub | 18 June 2014, 14:19:27 UTC | Fix generalize_mod_ w.r.t. non-generalized variables interacting with modified ones. | 18 June 2014, 14:19:27 UTC |
439c20d | Pierre-Yves Strub | 18 June 2014, 12:32:07 UTC | XDG | 18 June 2014, 12:32:07 UTC |
c7ed99b | Pierre-Yves Strub | 17 June 2014, 12:38:16 UTC | Moved out fortune from EasyCrypt + XDG aware config files. | 17 June 2014, 12:38:25 UTC |
a269bac | Pierre-Yves Strub | 17 June 2014, 08:48:38 UTC | Make EasyCrypt display a copyright in interactive mode. | 17 June 2014, 12:38:25 UTC |
62313ff | Francois Dupressoir | 16 June 2014, 13:00:38 UTC | Stabilizing smt call. | 16 June 2014, 14:30:37 UTC |
3c46215 | Benjamin Gregoire | 16 June 2014, 13:56:42 UTC | add variable projection for concrete glob | 16 June 2014, 13:56:42 UTC |
47dc86d | Benjamin Gregoire | 16 June 2014, 11:45:48 UTC | change and add lemmas | 16 June 2014, 11:45:48 UTC |
73924ca | Benjamin Gregoire | 16 June 2014, 11:45:27 UTC | ensure that algebra tactic can be applied | 16 June 2014, 11:45:27 UTC |
616e77d | Benjamin Gregoire | 12 June 2014, 17:13:30 UTC | Fixing bug in algebra | 12 June 2014, 17:13:30 UTC |
96cd363 | Benjamin Gregoire | 12 June 2014, 17:11:49 UTC | Fixing bug in syntaxification of ring and field | 12 June 2014, 17:11:49 UTC |
050b8e2 | Benjamin Gregoire | 11 June 2014, 10:55:37 UTC | add error message for fel tactic (require Sum) | 11 June 2014, 10:55:37 UTC |
48b5c5a | Benjamin Gregoire | 11 June 2014, 10:27:55 UTC | inline works modulo conversion of path. | 11 June 2014, 10:28:15 UTC |
97df9c6 | Benjamin Gregoire | 10 June 2014, 11:03:15 UTC | reduce the number of generated hypothesis in algebra. | 11 June 2014, 10:28:15 UTC |
4099245 | Francois Dupressoir | 11 June 2014, 10:09:48 UTC | Normalizing procedure names in FEL. Credit (and blame) should go to Benjamin. | 11 June 2014, 10:09:48 UTC |
b4acc44 | Pierre-Yves Strub | 10 June 2014, 11:00:04 UTC | Add missing memories in phl while tactic. | 10 June 2014, 11:00:12 UTC |
2b31339 | Benjamin Gregoire | 10 June 2014, 10:52:53 UTC | Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt/easycrypt into 1.0 | 10 June 2014, 10:52:53 UTC |
651c9ac | Benjamin Gregoire | 10 June 2014, 10:52:39 UTC | Fix bug in algebra | 10 June 2014, 10:52:39 UTC |
04757ca | Benjamin Gregoire | 10 June 2014, 10:47:23 UTC | Fix the previous « Fix internal symmetry tactic « . | 10 June 2014, 10:47:23 UTC |
140a5a1 | Pierre-Yves Strub | 10 June 2014, 08:38:39 UTC | Section can now be named section Foo. ... end section Foo. | 10 June 2014, 08:38:39 UTC |
8f516ed | Pierre-Yves Strub | 10 June 2014, 08:09:54 UTC | Error message when hi-level [reflexivity] tactic fails. Fix #17009. | 10 June 2014, 08:09:54 UTC |
606b7a2 | Pierre-Yves Strub | 10 June 2014, 07:47:29 UTC | Fix internal symmetry tactic. | 10 June 2014, 07:47:29 UTC |
08a24e5 | Pierre-Yves Strub | 09 June 2014, 14:51:57 UTC | Fix bug in ring instances cloning Abstract operators path were not updated. | 09 June 2014, 14:52:06 UTC |
4708315 | Pierre-Yves Strub | 05 June 2014, 14:27:46 UTC | Refactor AST for module declaration | 09 June 2014, 14:52:06 UTC |
b324e80 | Benjamin Gregoire | 05 June 2014, 14:16:52 UTC | algebra now try to solve inequality generated by fieldeq. | 05 June 2014, 14:16:52 UTC |
86c3829 | Benjamin Gregoire | 05 June 2014, 12:26:47 UTC | Remove duplicated subgoal in fieldeq. | 05 June 2014, 12:26:47 UTC |
ec23837 | Benjamin Gregoire | 05 June 2014, 12:19:16 UTC | Extend strongRing with field. | 05 June 2014, 12:19:16 UTC |
607a077 | Benjamin Gregoire | 05 June 2014, 11:32:26 UTC | Fixing bug in fieldeq. | 05 June 2014, 11:32:26 UTC |
bbfad45 | Benjamin Gregoire | 05 June 2014, 09:09:31 UTC | Restore and improve StrongRing | 05 June 2014, 09:09:31 UTC |
6a536e6 | Benjamin Gregoire | 04 June 2014, 14:46:08 UTC | remove the need to use « declare rewrite foo ». check that no clash exists between axiom and base rewrite | 04 June 2014, 14:46:08 UTC |
8d2eba9 | Benjamin Gregoire | 04 June 2014, 13:47:33 UTC | add possibility to use rewrite base in rewrite | 04 June 2014, 13:47:33 UTC |
9637d1a | Benjamin Gregoire | 04 June 2014, 12:52:11 UTC | Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt/easycrypt into 1.0 | 04 June 2014, 12:52:11 UTC |
a6285ac | Benjamin Gregoire | 04 June 2014, 12:52:03 UTC | add base for rewrite | 04 June 2014, 12:52:03 UTC |
d2afd01 | Pierre-Yves Strub | 04 June 2014, 09:49:10 UTC | autorewrite | 04 June 2014, 09:51:56 UTC |
3c9b043 | Francois Dupressoir | 29 May 2014, 06:45:01 UTC | Adding the OCaml patch to the MANIFEST. | 29 May 2014, 06:45:01 UTC |
bbfb34f | Francois Dupressoir | 27 May 2014, 08:47:33 UTC | smt in some unit test. | 27 May 2014, 08:47:33 UTC |
323cb9e | Pierre-Yves Strub | 22 May 2014, 05:11:26 UTC | [case/elim] handle tuple. | 22 May 2014, 05:11:26 UTC |
afe6f79 | Pierre-Yves Strub | 21 May 2014, 15:32:09 UTC | Better error message when case/elim is not applicable. | 21 May 2014, 15:32:09 UTC |
0eff9c7 | Pierre-Yves Strub | 21 May 2014, 15:22:14 UTC | [print glob] now works on module instantiations. | 21 May 2014, 15:22:14 UTC |
d60ba6b | Pierre-Yves Strub | 21 May 2014, 15:12:10 UTC | Add a top level command for printing module globals Command is [print glob $mpath] | 21 May 2014, 15:12:10 UTC |
2231d00 | Pierre-Yves Strub | 20 May 2014, 14:41:43 UTC | Error messages for proof-terms application. | 20 May 2014, 14:41:43 UTC |
d136561 | Pierre-Yves Strub | 20 May 2014, 14:17:48 UTC | Fix printing a tuple projections. | 20 May 2014, 14:17:48 UTC |
8da987c | Pierre-Yves Strub | 19 May 2014, 13:33:06 UTC | Internal refactoring: lexer can now return a list of lexems This should help better parsing operators. | 19 May 2014, 13:33:06 UTC |
677e0e3 | Pierre-Yves Strub | 19 May 2014, 12:41:35 UTC | [nosmt] for axiomatized operators. | 19 May 2014, 12:41:35 UTC |
754ddfd | Pierre-Yves Strub | 18 May 2014, 17:28:37 UTC | When in local mode, add the bin/ directory of the first toolchain to the system PATH. | 18 May 2014, 17:28:37 UTC |
8078c81 | Pierre-Yves Strub | 18 May 2014, 08:48:55 UTC | Update toolchain to OCaml 4.01 & Opam 1.1.0 Pactching OCaml s.t. it compiles on Mac. | 18 May 2014, 08:48:55 UTC |
041fd55 | Benjamin Gregoire | 16 May 2014, 14:50:10 UTC | instantiate hybrid with DDH | 16 May 2014, 14:50:10 UTC |
da8f694 | Benjamin Gregoire | 16 May 2014, 13:45:21 UTC | Fix durty commit | 16 May 2014, 13:45:21 UTC |
136f660 | Benjamin Gregoire | 16 May 2014, 13:39:14 UTC | Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt/easycrypt into 1.0 | 16 May 2014, 13:39:14 UTC |
14a525f | Benjamin Gregoire | 16 May 2014, 13:39:00 UTC | more on hybrid | 16 May 2014, 13:39:00 UTC |
429ebad | Pierre-Yves Strub | 06 May 2014, 15:45:11 UTC | Remove staled roadmap - we have a web-based roadmap now. | 06 May 2014, 15:45:18 UTC |
281345d | Pierre-Yves Strub | 25 April 2014, 13:31:03 UTC | Fix test suite (rnd) | 25 April 2014, 13:31:03 UTC |
2220147 | Pierre-Yves Strub | 25 April 2014, 13:16:07 UTC | Fix capture of variables in substitution. | 25 April 2014, 13:16:07 UTC |
572c2ad | Pierre-Yves Strub | 25 April 2014, 13:01:04 UTC | Allow upper-case identifiers in [pose]. | 25 April 2014, 13:01:04 UTC |
e6a7dec | Pierre-Yves Strub | 24 April 2014, 08:03:03 UTC | Factor code w.r.t the sections mechanism to its own module. | 24 April 2014, 14:52:17 UTC |
9c195bd | Francois Dupressoir | 24 April 2014, 12:38:14 UTC | Fixing examples after important bugfix. | 24 April 2014, 12:38:14 UTC |
d024233 | Pierre-Yves Strub | 23 April 2014, 16:57:21 UTC | Fix f_andsa/f_orsa associativity | 23 April 2014, 16:57:21 UTC |
a408a1d | Pierre-Yves Strub | 23 April 2014, 14:45:39 UTC | Fix error message in intro (was asserting false) | 23 April 2014, 14:45:39 UTC |
541ff05 | Pierre-Yves Strub | 23 April 2014, 09:57:20 UTC | Rework [rnd] tactic This fixes a bug in [rnd] when one of two distributions where empty. | 23 April 2014, 10:06:40 UTC |
f16c9a3 | Francois Dupressoir | 10 April 2014, 21:09:46 UTC | Silencing LaTeX errors due to example obsolescence. | 10 April 2014, 21:09:46 UTC |
0bf9015 | Francois Dupressoir | 09 April 2014, 15:56:36 UTC | Stabilizing smt calls in PRG example. | 09 April 2014, 15:56:36 UTC |
a6afa4f | Pierre-Yves Strub | 09 April 2014, 13:09:48 UTC | Why3 term alpha-convertibility + related maps refactored in [EcWhy3Conv]. | 09 April 2014, 13:09:48 UTC |
47b4be7 | Pierre-Yves Strub | 09 April 2014, 13:03:56 UTC | Why3 refactoring: subdirectory why3/ created and relevant files moved. | 09 April 2014, 13:03:56 UTC |
789a516 | Pierre-Yves Strub | 09 April 2014, 12:53:18 UTC | In [subst], don't clear a variable when it is defined. | 09 April 2014, 12:53:18 UTC |
b7e75c7 | Pierre-Yves Strub | 09 April 2014, 12:31:54 UTC | Fix #17009 (better error messages) | 09 April 2014, 12:31:54 UTC |
bdf003c | Francois Dupressoir | 08 April 2014, 14:22:30 UTC | Updating PRG example (some bad smt for some reason). | 08 April 2014, 14:22:30 UTC |
fafd8fd | Francois Dupressoir | 08 April 2014, 14:07:42 UTC | Updating Plug_and_Pray. | 08 April 2014, 14:07:42 UTC |
dff3779 | Pierre-Yves Strub | 08 April 2014, 12:23:19 UTC | Fix compilation issue with OCaml 4.00.x | 08 April 2014, 12:23:19 UTC |
6fe0ea9 | Pierre-Yves Strub | 07 April 2014, 14:29:35 UTC | Remove dead code form EcLogic/EcBaseLogic. | 07 April 2014, 14:29:35 UTC |
3423f87 | Pierre-Yves Strub | 12 March 2014, 17:48:52 UTC | Refactor all tactics using new proof engine. + disconnect type classes + reconnect legacy ring | 07 April 2014, 12:26:06 UTC |
d4b1966 | Pierre-Yves Strub | 06 March 2014, 21:35:53 UTC | Split tacticals engine in its own module. | 04 April 2014, 13:22:40 UTC |
ac5be62 | Pierre-Yves Strub | 06 March 2014, 21:09:25 UTC | Killed warnings (unused variables) | 04 April 2014, 13:22:40 UTC |
3206dfe | Francois Dupressoir | 03 April 2014, 10:21:21 UTC | Cleaning up the examples folder for distribution. | 03 April 2014, 10:21:25 UTC |
9c86b98 | Pierre-Yves Strub | 03 April 2014, 10:19:34 UTC | Add a global -timeout flag + timeout=0 => infinite timeout. | 03 April 2014, 10:19:34 UTC |
2cef9f2 | Francois Dupressoir | 01 April 2014, 17:40:53 UTC | Adding some useful axioms and lemmas on exponents. | 01 April 2014, 17:40:53 UTC |