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 |
8b15f74 | Benjamin Gregoire | 01 April 2014, 08:10:56 UTC | Add univ in AWord | 01 April 2014, 08:10:56 UTC |
6df81b6 | Benjamin Gregoire | 01 April 2014, 07:58:40 UTC | add product of two and 3 sets | 01 April 2014, 07:58:40 UTC |
e43821c | Francois Dupressoir | 26 March 2014, 09:22:08 UTC | Reverting undesired changes to Means. The proofs are still broken, but they will at least work again when field and ring are fixed. | 26 March 2014, 09:22:08 UTC |
ec6abbf | Francois Dupressoir | 25 March 2014, 21:51:20 UTC | I hate subdistributions. | 25 March 2014, 21:51:20 UTC |
45f3f0d | Francois Dupressoir | 25 March 2014, 13:52:42 UTC | A useful axiom on the unicity of the uniform distribution given a finite set. | 25 March 2014, 13:52:42 UTC |
b2728cf | Francois Dupressoir | 24 March 2014, 11:27:03 UTC | ROM: Adding a useful initialization lemma. | 24 March 2014, 11:27:03 UTC |
70991a7 | Francois Dupressoir | 21 March 2014, 17:41:14 UTC | Fixing broken proof (ringeq). | 21 March 2014, 17:41:14 UTC |
6f77de0 | Francois Dupressoir | 21 March 2014, 17:36:58 UTC | Fixing a broken proof (broken fieldeq). | 21 March 2014, 17:36:58 UTC |
2aa700f | Francois Dupressoir | 21 March 2014, 17:28:39 UTC | ROM extended with some high-level transitions (up to collision on a given call, and abstract up to bad). Cleaning up examples directory. | 21 March 2014, 17:29:04 UTC |
9fc06a4 | Francois Dupressoir | 18 March 2014, 14:27:33 UTC | A generic-argument-based version of Hashed El Gamal -> CDH. | 18 March 2014, 14:27:33 UTC |
2271abe | Francois Dupressoir | 17 March 2014, 22:18:55 UTC | Hashed El Gamal ported over. No abstract proof steps. | 17 March 2014, 22:18:55 UTC |
555ded8 | Francois Dupressoir | 17 March 2014, 20:01:42 UTC | On the way to adapting Hashed El Gamal. CDH in 1.0, with bug workarounds galore! | 17 March 2014, 20:01:42 UTC |
1b2f432 | Francois Dupressoir | 11 March 2014, 08:53:31 UTC | Keywords | 11 March 2014, 08:53:31 UTC |
7b8628a | Pierre-Yves Strub | 06 March 2014, 21:06:04 UTC | Dead code removed ([claim]) | 06 March 2014, 21:06:04 UTC |
750bf41 | Pierre-Yves Strub | 06 March 2014, 21:00:20 UTC | Flow tcenv/tcenv1 types through the whole stack. A tactic is now a function from tcenv1 to tcenv. | 06 March 2014, 21:00:20 UTC |
10e469f | Pierre-Yves Strub | 05 March 2014, 09:15:45 UTC | Statically enforce that a goal has no subgoals. | 05 March 2014, 09:15:45 UTC |
fe5a5ae | Pierre-Yves Strub | 04 March 2014, 15:19:43 UTC | Phl [fun] duplicated (old/new engine) | 04 March 2014, 15:19:43 UTC |
cd9e600 | Pierre-Yves Strub | 04 March 2014, 15:11:24 UTC | Change type for external proof nodes: the list of depending proof handles is explicit. | 04 March 2014, 15:11:24 UTC |
8bf8166 | Pierre-Yves Strub | 04 March 2014, 08:58:17 UTC | Export more low-level elim. tactics of the new proof engine. | 04 March 2014, 08:58:17 UTC |
19bb8ea | Pierre-Yves Strub | 04 March 2014, 08:57:53 UTC | Parse-tree for [fun] related tactics factored. | 04 March 2014, 08:57:53 UTC |
c2077f8 | Pierre-Yves Strub | 04 March 2014, 08:56:27 UTC | New accessors for proof environments. | 04 March 2014, 08:56:27 UTC |
3eecc72 | Pierre-Yves Strub | 04 March 2014, 08:53:35 UTC | conseq in new proof engine: module renaming. | 04 March 2014, 08:53:35 UTC |
bc65216 | Pierre-Yves Strub | 03 March 2014, 16:57:08 UTC | Low level t_case in new proof engine. | 03 March 2014, 16:57:08 UTC |
341e546 | Pierre-Yves Strub | 03 March 2014, 16:40:53 UTC | Loew-level intro/elim in new engine. | 03 March 2014, 16:40:53 UTC |
5522365 | Pierre-Yves Strub | 03 March 2014, 09:32:38 UTC | In t_rewrite, check the proof term, even when the set of possible occurences is empty. | 03 March 2014, 09:32:38 UTC |
4d4a8b5 | Pierre-Yves Strub | 03 March 2014, 09:30:26 UTC | Low/Hi cut. | 03 March 2014, 09:30:26 UTC |
d5a5f86 | Pierre-Yves Strub | 01 March 2014, 10:29:53 UTC | Fix of the proof for t_true. | 01 March 2014, 10:29:53 UTC |
804d3c6 | Pierre-Yves Strub | 28 February 2014, 20:40:09 UTC | Hi-level core rewriting in new proof engine. | 28 February 2014, 20:40:09 UTC |
41eef91 | Pierre-Yves Strub | 28 February 2014, 16:42:54 UTC | Low level rewrite in new proof-engine. | 28 February 2014, 16:42:54 UTC |
380d406 | Pierre-Yves Strub | 28 February 2014, 15:39:44 UTC | EcMetaProg -> EcMatching | 28 February 2014, 15:44:33 UTC |
434e522 | Pierre-Yves Strub | 28 February 2014, 15:38:59 UTC | Remove instruction pattern matching (dead code). | 28 February 2014, 15:38:59 UTC |
72d815a | Pierre-Yves Strub | 28 February 2014, 10:38:47 UTC | New engine refactored. | 28 February 2014, 10:38:47 UTC |
1eb3610 | Pierre-Yves Strub | 27 February 2014, 20:29:02 UTC | low/hi-level apply in new proof engine. | 27 February 2014, 20:29:02 UTC |