| 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 |
| 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 |
