| a79f9ae | Pierre-Yves Strub | 08 July 2014, 09:43:21 UTC | Fix bug w.r.t. _tools presence detection. | 08 July 2014, 09:43:21 UTC |
| 423a921 | Pierre-Yves Strub | 08 July 2014, 09:24:15 UTC | Add support for local hypothesis. | 08 July 2014, 09:24:15 UTC |
| 9c7b05e | Pierre-Yves Strub | 07 July 2014, 21:18:11 UTC | Don't erase status line when displaying an error message. | 07 July 2014, 21:18:11 UTC |
| 3767cd4 | Pierre-Yves Strub | 07 July 2014, 21:16:35 UTC | Display line number in terminal. | 07 July 2014, 21:16:35 UTC |
| df12895 | Pierre-Yves Strub | 07 July 2014, 21:13:08 UTC | Proof scripts not started with [proof] are now in strict mode. | 07 July 2014, 21:13:08 UTC |
| ff7b8e6 | Pierre-Yves Strub | 07 July 2014, 21:08:06 UTC | Keywords | 07 July 2014, 21:08:06 UTC |
| 0676384 | Francois Dupressoir | 07 July 2014, 20:07:17 UTC | More useful div_def. | 07 July 2014, 20:07:40 UTC |
| 161a116 | Pierre-Yves Strub | 07 July 2014, 19:31:55 UTC | Fix extraction pp regarding parenthesis. | 07 July 2014, 19:31:55 UTC |
| 8f72bf8 | Pierre-Yves Strub | 07 July 2014, 16:25:28 UTC | In extraction, fix directories creation. | 07 July 2014, 16:25:28 UTC |
| de895b4 | Pierre-Yves Strub | 07 July 2014, 15:25:35 UTC | autogen.sh for extraction. | 07 July 2014, 15:25:35 UTC |
| bc538cb | Pierre-Yves Strub | 07 July 2014, 15:22:10 UTC | Makefile (oasis) for extraction support library. | 07 July 2014, 15:22:28 UTC |
| 875a92b | Pierre-Yves Strub | 07 July 2014, 15:09:13 UTC | cygwin -> CYGWIN | 07 July 2014, 15:09:13 UTC |
| 680d5b0 | Pierre-Yves Strub | 07 July 2014, 15:02:32 UTC | Don't use non-standard option of uname in Makefile | 07 July 2014, 15:02:32 UTC |
| 30a36fb | Pierre-Yves Strub | 07 July 2014, 14:43:57 UTC | In extraction, create output directory if it doesn't exist. | 07 July 2014, 14:43:57 UTC |
| e28d5da | Pierre-Yves Strub | 07 July 2014, 14:36:40 UTC | Extraction of tuples projections. | 07 July 2014, 14:36:40 UTC |
| e4c545f | Pierre-Yves Strub | 07 July 2014, 14:20:08 UTC | Explain restrictions errors (in UI) | 07 July 2014, 14:20:08 UTC |
| 205e287 | Benjamin Gregoire | 07 July 2014, 14:10:14 UTC | explain restriction error | 07 July 2014, 14:10:32 UTC |
| 4a29da9 | Pierre-Yves Strub | 07 July 2014, 10:46:49 UTC | Fix pattern matching w.r.t. matching bound variables The current pattern matching algorithm is not meant to support this at this time. | 07 July 2014, 10:46:55 UTC |
| 9319023 | Benjamin Gregoire | 07 July 2014, 09:40:33 UTC | add lemmas and axioms | 07 July 2014, 09:40:49 UTC |
| 5b61bec | Pierre-Yves Strub | 06 July 2014, 17:08:07 UTC | Some tweaks for perfs. | 06 July 2014, 17:08:07 UTC |
| fc553db | Pierre-Yves Strub | 06 July 2014, 15:16:25 UTC | Accept sub-proofterms. | 06 July 2014, 15:16:25 UTC |
| 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 |
