36a5c0d | Pierre-Yves Strub | 06 July 2014, 11:27:19 UTC | Fix behaviour of [progress [delta:split]] | 06 July 2014, 11:27:19 UTC |
5605003 | Pierre-Yves Strub | 06 July 2014, 11:14:37 UTC | In [progress] options, [-] now unset the option (was setting it) | 06 July 2014, 11:14:37 UTC |
dfd171b | Pierre-Yves Strub | 06 July 2014, 10:18:17 UTC | Fix parsing issue for [progress] options | 06 July 2014, 10:18:17 UTC |
0e79d41 | Pierre-Yves Strub | 06 July 2014, 09:03:38 UTC | Properly clean-up status line in terminal. | 06 July 2014, 09:03:45 UTC |
154ca63 | Pierre-Yves Strub | 06 July 2014, 07:52:16 UTC | Don't use non-standard options of uname + update README. | 06 July 2014, 07:52:16 UTC |
ea61948 | Pierre-Yves Strub | 06 July 2014, 07:32:45 UTC | Restore [delta] option for [progress] The option can now be refined with two modifiers (case/split) seperated with a colon. E.g. [progress [delta:split]] By default, [delta:split] is on, [delta:case] is off. Also, negative options are now given using the [-] mark. E.g. [progress [-delta]] | 06 July 2014, 07:34:41 UTC |
7caf0b7 | Pierre-Yves Strub | 06 July 2014, 06:52:39 UTC | Revert "Revert "[nodelta] for [progress] (2nd round)"" This reverts commit dd612bac9eea5f278af41c0db869a8e28e56641a. | 06 July 2014, 06:52:39 UTC |
fbb1af8 | Pierre-Yves Strub | 06 July 2014, 06:51:43 UTC | in [eager], use lazy error message printing. | 06 July 2014, 06:51:43 UTC |
dd612ba | Benjamin Gregoire | 05 July 2014, 22:49:31 UTC | Revert "[nodelta] for [progress] (2nd round)" This reverts commit ebafbc92ad9b52ae775ab3bd4f9ddbb32bd51e73. | 05 July 2014, 22:49:31 UTC |
50c7068 | Benjamin Gregoire | 05 July 2014, 20:24:44 UTC | Improve error message. | 05 July 2014, 22:14:36 UTC |
bb592db | Benjamin Gregoire | 04 July 2014, 13:13:36 UTC | add SFproj | 05 July 2014, 22:14:36 UTC |
ebafbc9 | Pierre-Yves Strub | 05 July 2014, 22:13:30 UTC | [nodelta] for [progress] (2nd round) | 05 July 2014, 22:13:30 UTC |
7c527a4 | Pierre-Yves Strub | 05 July 2014, 20:23:48 UTC | [delta/nodelta] options for progress. | 05 July 2014, 20:23:48 UTC |
7daf7f9 | Pierre-Yves Strub | 05 July 2014, 16:57:44 UTC | Allow empty case intro-pattern (i.e. do a case, intro nothing) | 05 July 2014, 16:57:44 UTC |
3fb5602 | Pierre-Yves Strub | 05 July 2014, 12:20:08 UTC | [rewrite smt]: call [smt]. | 05 July 2014, 12:20:08 UTC |
a7bea72 | Pierre-Yves Strub | 04 July 2014, 12:43:41 UTC | Remove '?' from the operators characters set. | 04 July 2014, 12:43:41 UTC |
722dd00 | Pierre-Yves Strub | 04 July 2014, 12:40:13 UTC | Support repeater in rewrite /o (unfolding) | 04 July 2014, 12:40:13 UTC |
fce7110 | Pierre-Yves Strub | 04 July 2014, 12:24:28 UTC | Allow reverse rewriting in multi-rewrite rules. Syntax: rewrite (-a, -b), i.e. adding an inner [-] sign where needed. | 04 July 2014, 12:24:28 UTC |
13eacf2 | Pierre-Yves Strub | 04 July 2014, 12:10:08 UTC | Fix to the [inline] tactic. Inline was using an xpath substitution instead of a prog_var one, leading to assertion failure when trying to normalize a prog_var path as a function path. | 04 July 2014, 12:10:18 UTC |
7044e28 | Benjamin Gregoire | 04 July 2014, 10:38:21 UTC | improve previous patch | 04 July 2014, 11:05:17 UTC |
a10adcf | Benjamin Gregoire | 04 July 2014, 10:38:21 UTC | improve previous patch | 04 July 2014, 10:52:33 UTC |
7f3443c | Benjamin Gregoire | 04 July 2014, 10:31:58 UTC | catch exception and raise error msg | 04 July 2014, 10:52:33 UTC |
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 |