https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
a79f9ae Fix bug w.r.t. _tools presence detection. 08 July 2014, 09:43 UTC
423a921 Add support for local hypothesis. 08 July 2014, 09:24 UTC
9c7b05e Don't erase status line when displaying an error message. 07 July 2014, 21:18 UTC
3767cd4 Display line number in terminal. 07 July 2014, 21:16 UTC
df12895 Proof scripts not started with [proof] are now in strict mode. 07 July 2014, 21:13 UTC
ff7b8e6 Keywords 07 July 2014, 21:08 UTC
0676384 More useful div_def. 07 July 2014, 20:07 UTC
161a116 Fix extraction pp regarding parenthesis. 07 July 2014, 19:31 UTC
8f72bf8 In extraction, fix directories creation. 07 July 2014, 16:25 UTC
de895b4 autogen.sh for extraction. 07 July 2014, 15:25 UTC
bc538cb Makefile (oasis) for extraction support library. 07 July 2014, 15:22 UTC
875a92b cygwin -> CYGWIN 07 July 2014, 15:09 UTC
680d5b0 Don't use non-standard option of uname in Makefile 07 July 2014, 15:02 UTC
30a36fb In extraction, create output directory if it doesn't exist. 07 July 2014, 14:43 UTC
e28d5da Extraction of tuples projections. 07 July 2014, 14:36 UTC
e4c545f Explain restrictions errors (in UI) 07 July 2014, 14:20 UTC
205e287 explain restriction error 07 July 2014, 14:10 UTC
4a29da9 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 UTC
9319023 add lemmas and axioms 07 July 2014, 09:40 UTC
5b61bec Some tweaks for perfs. 06 July 2014, 17:08 UTC
fc553db Accept sub-proofterms. 06 July 2014, 15:16 UTC
36a5c0d Fix behaviour of [progress [delta:split]] 06 July 2014, 11:27 UTC
5605003 In [progress] options, [-] now unset the option (was setting it) 06 July 2014, 11:14 UTC
dfd171b Fix parsing issue for [progress] options 06 July 2014, 10:18 UTC
0e79d41 Properly clean-up status line in terminal. 06 July 2014, 09:03 UTC
154ca63 Don't use non-standard options of uname + update README. 06 July 2014, 07:52 UTC
ea61948 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 UTC
7caf0b7 Revert "Revert "[nodelta] for [progress] (2nd round)"" This reverts commit dd612bac9eea5f278af41c0db869a8e28e56641a. 06 July 2014, 06:52 UTC
fbb1af8 in [eager], use lazy error message printing. 06 July 2014, 06:51 UTC
dd612ba Revert "[nodelta] for [progress] (2nd round)" This reverts commit ebafbc92ad9b52ae775ab3bd4f9ddbb32bd51e73. 05 July 2014, 22:49 UTC
50c7068 Improve error message. 05 July 2014, 22:14 UTC
bb592db add SFproj 05 July 2014, 22:14 UTC
ebafbc9 [nodelta] for [progress] (2nd round) 05 July 2014, 22:13 UTC
7c527a4 [delta/nodelta] options for progress. 05 July 2014, 20:23 UTC
7daf7f9 Allow empty case intro-pattern (i.e. do a case, intro nothing) 05 July 2014, 16:57 UTC
3fb5602 [rewrite smt]: call [smt]. 05 July 2014, 12:20 UTC
a7bea72 Remove '?' from the operators characters set. 04 July 2014, 12:43 UTC
722dd00 Support repeater in rewrite /o (unfolding) 04 July 2014, 12:40 UTC
fce7110 Allow reverse rewriting in multi-rewrite rules. Syntax: rewrite (-a, -b), i.e. adding an inner [-] sign where needed. 04 July 2014, 12:24 UTC
13eacf2 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 UTC
7044e28 improve previous patch 04 July 2014, 11:05 UTC
a10adcf improve previous patch 04 July 2014, 10:52 UTC
7f3443c catch exception and raise error msg 04 July 2014, 10:52 UTC
b1c2c84 Tuples equality simplification now uses symmetric equality. 04 July 2014, 10:48 UTC
7f70b66 Reduction of equality between concrete tuples. 04 July 2014, 10:25 UTC
dee4e63 Dead code removal 02 July 2014, 10:17 UTC
72b59f2 [make toolchain] now works under cygwin (32) 01 July 2014, 20:58 UTC
1764a53 Test for forward apply in intros. 01 July 2014, 19:35 UTC
f0f2a2b Forward apply in intro pattern. Syntax: move=> /pf. 01 July 2014, 19:28 UTC
08b8ffe Marking a controversial lemma as nosmt. 01 July 2014, 12:56 UTC
cf12dc4 Test for intro-pattern <<- & ->>. 26 June 2014, 19:35 UTC
2b63167 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 UTC
3fbffa7 Add new arrows: <<- && ->> 26 June 2014, 18:40 UTC
7b3b04d Add an elimintation principle of the unit type. 26 June 2014, 10:05 UTC
35d7517 Search for the elimintation principle using the head-normal form of a type. 26 June 2014, 09:55 UTC
9f3d473 Negative occurences selection. 26 June 2014, 09:16 UTC
f12cf14 Don't crash when using [proof] outside of a proof. 26 June 2014, 09:11 UTC
667ec96 Fix notification w.r.t. lemmas / axioms. 25 June 2014, 17:13 UTC
3487b1d Adding rng operator. 24 June 2014, 16:29 UTC
266d5c9 Add trivial module in Pair 23 June 2014, 14:28 UTC
ea70757 Fixing part of the bug 17029. 23 June 2014, 14:28 UTC
2aaca80 Pattern matching now supports meta-var for memories. 22 June 2014, 23:05 UTC
fdc7039 Update copyright for command line interface. 22 June 2014, 22:08 UTC
3c18074 Update copyright on all source files. 22 June 2014, 22:02 UTC
35acf25 Script for setting / updating copyright on source files. 22 June 2014, 22:01 UTC
bb4b80a Updating keywords. 20 June 2014, 09:54 UTC
997d5d4 Fix theory IRing 19 June 2014, 07:49 UTC
8bc5765 Fixing bug #17027 and #17028 19 June 2014, 07:49 UTC
6a7878b Fixing ROM and test after bugfix. The old test should be used as negative test. 18 June 2014, 14:41 UTC
138c4ab Fix generalize_mod_ w.r.t. non-generalized variables interacting with modified ones. 18 June 2014, 14:19 UTC
439c20d XDG 18 June 2014, 12:32 UTC
c7ed99b Moved out fortune from EasyCrypt + XDG aware config files. 17 June 2014, 12:38 UTC
a269bac Make EasyCrypt display a copyright in interactive mode. 17 June 2014, 12:38 UTC
62313ff Stabilizing smt call. 16 June 2014, 14:30 UTC
3c46215 add variable projection for concrete glob 16 June 2014, 13:56 UTC
47dc86d change and add lemmas 16 June 2014, 11:45 UTC
73924ca ensure that algebra tactic can be applied 16 June 2014, 11:45 UTC
616e77d Fixing bug in algebra 12 June 2014, 17:13 UTC
96cd363 Fixing bug in syntaxification of ring and field 12 June 2014, 17:11 UTC
050b8e2 add error message for fel tactic (require Sum) 11 June 2014, 10:55 UTC
48b5c5a inline works modulo conversion of path. 11 June 2014, 10:28 UTC
97df9c6 reduce the number of generated hypothesis in algebra. 11 June 2014, 10:28 UTC
4099245 Normalizing procedure names in FEL. Credit (and blame) should go to Benjamin. 11 June 2014, 10:09 UTC
b4acc44 Add missing memories in phl while tactic. 10 June 2014, 11:00 UTC
2b31339 Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt/easycrypt into 1.0 10 June 2014, 10:52 UTC
651c9ac Fix bug in algebra 10 June 2014, 10:52 UTC
04757ca Fix the previous « Fix internal symmetry tactic «  . 10 June 2014, 10:47 UTC
140a5a1 Section can now be named section Foo. ... end section Foo. 10 June 2014, 08:38 UTC
8f516ed Error message when hi-level [reflexivity] tactic fails. Fix #17009. 10 June 2014, 08:09 UTC
606b7a2 Fix internal symmetry tactic. 10 June 2014, 07:47 UTC
08a24e5 Fix bug in ring instances cloning Abstract operators path were not updated. 09 June 2014, 14:52 UTC
4708315 Refactor AST for module declaration 09 June 2014, 14:52 UTC
b324e80 algebra now try to solve inequality generated by fieldeq. 05 June 2014, 14:16 UTC
86c3829 Remove duplicated subgoal in fieldeq. 05 June 2014, 12:26 UTC
ec23837 Extend strongRing with field. 05 June 2014, 12:19 UTC
607a077 Fixing bug in fieldeq. 05 June 2014, 11:32 UTC
bbfad45 Restore and improve StrongRing 05 June 2014, 09:09 UTC
6a536e6 remove the need to use « declare rewrite foo ». check that no clash exists between axiom and base rewrite   04 June 2014, 14:46 UTC
8d2eba9 add possibility to use rewrite base in rewrite 04 June 2014, 13:47 UTC
9637d1a Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt/easycrypt into 1.0 04 June 2014, 12:52 UTC
back to top