Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
05 April 2024, 19:20:55 UTC
sort by:
Revision Author Date Message Commit Date
592d84e Pierre-Yves Strub 09 December 2015, 15:21:49 UTC Improve matching of quantifiers. [fix #17277] 09 December 2015, 15:22:00 UTC
32e528c Pierre-Yves Strub 09 December 2015, 14:48:27 UTC Nits in bigops && lists. 09 December 2015, 14:48:27 UTC
eaff014 Pierre-Yves Strub 09 December 2015, 14:48:16 UTC New tactic: `suff`. Similar to `have`, but apply the optional tactic to the main goal, and swap the cut and the main goal when compared to `have`. 09 December 2015, 14:48:16 UTC
48f9f9f Benjamin Gregoire 09 December 2015, 11:09:54 UTC add Sample become abstract 09 December 2015, 11:11:10 UTC
990f751 Pierre-Yves Strub 09 December 2015, 11:04:25 UTC `bigi` is now a notation. 09 December 2015, 11:04:33 UTC
0701cb7 Pierre-Yves Strub 09 December 2015, 10:50:36 UTC `(-)` (Int/Real/Ring) is now an abbrev. 09 December 2015, 10:55:43 UTC
443d2a4 François Dupressoir 09 December 2015, 08:57:12 UTC Additions and typos in NewFMap. 09 December 2015, 10:51:23 UTC
4321103 Benjamin Gregoire 09 December 2015, 09:48:49 UTC conseq (_:P) stands for cones (_:_==>P). 09 December 2015, 10:51:22 UTC
30c2fd2 Benjamin Gregoire 09 December 2015, 09:07:44 UTC fixing previous merge ... 09 December 2015, 10:51:21 UTC
2bbc82f Benjamin Gregoire 09 December 2015, 08:55:30 UTC improve location and error message of NotAFunction. 09 December 2015, 10:51:20 UTC
29b9ac4 Pierre-Yves Strub 08 December 2015, 21:36:04 UTC Allow pruning abbrev. from abstract theories. 08 December 2015, 21:36:14 UTC
faae8f1 Pierre-Yves Strub 08 December 2015, 20:20:31 UTC Add an option to clear abbrev. when cloning. Syntax is `clear abbrev names+` + proof/renaming/clear can now be interleaved. 08 December 2015, 20:21:34 UTC
29d5540 Pierre-Yves Strub 08 December 2015, 19:20:53 UTC Fix notations import + allow partial appl. of abbrev. 08 December 2015, 19:22:38 UTC
3f68858 Pierre-Yves Strub 08 December 2015, 14:13:39 UTC Abbreviation are now parsed and expanded. Abbrev. are now assumed to work fully. 08 December 2015, 14:16:04 UTC
009c962 Pierre-Yves Strub 08 December 2015, 09:39:34 UTC Top-level assumption duplication does not require a name anymore. The syntax is `move=> ^`. This i-p duplicates the top-assumption, pushing the duplicate as the new top-assumption. This strictly generalizes the `move=> ^h` syntax. 08 December 2015, 10:10:02 UTC
3fd09bb Pierre-Yves Strub 08 December 2015, 09:27:05 UTC Clear generalization pattern. Syntax is `move: {id1 ... idn}` and can be followed by regular generalization patterns. 08 December 2015, 10:08:46 UTC
0de39c7 Pierre-Yves Strub 07 December 2015, 20:42:07 UTC Internal refactoring: operator selection. 07 December 2015, 20:43:16 UTC
f8e5bd6 Pierre-Yves Strub 07 December 2015, 19:20:16 UTC In pp, use active memory when translating an expr to a form. 07 December 2015, 19:36:37 UTC
f0e00b0 Pierre-Yves Strub 06 December 2015, 21:41:17 UTC Fix pretty-printing of polymorphic abbrev. 06 December 2015, 21:41:26 UTC
44d46e9 Pierre-Yves Strub 06 December 2015, 20:14:15 UTC Pretty-printing notations. But still not parsing them :) 06 December 2015, 20:14:23 UTC
c279481 Pierre-Yves Strub 06 December 2015, 18:10:24 UTC Add new options to the matching algo: - fix: fm_conv is now respected - new: fm_horder: when false no higher-order matching is performed. 06 December 2015, 18:10:37 UTC
6177a35 Pierre-Yves Strub 06 December 2015, 17:56:01 UTC Register notations into a database located in the env. 06 December 2015, 17:56:12 UTC
9de0f56 Pierre-Yves Strub 04 December 2015, 11:35:58 UTC Nits in pretty-printer. 04 December 2015, 11:36:29 UTC
c35ae8f Pierre-Yves Strub 04 December 2015, 11:34:49 UTC Better lemmas clearing strategy. + update stdlib w.r.t. this new strategy. 04 December 2015, 11:36:27 UTC
999775a Pierre-Yves Strub 04 December 2015, 09:17:14 UTC `ring` is now callable from `rewrite`. Syntax is `rewrite #ring`. The syntax `rewrite #tactic` might be generic in a near future, but currently, only `ring` is plugged-in. 04 December 2015, 09:21:55 UTC
a241ea1 Pierre-Yves Strub 04 December 2015, 08:10:29 UTC Replug pp for proof-term typing errors. 04 December 2015, 09:21:55 UTC
3679fcd Pierre-Yves Strub 04 December 2015, 07:59:51 UTC List: last_rev. 04 December 2015, 09:21:55 UTC
51b6ca3 Pierre-Yves Strub 04 December 2015, 07:59:43 UTC List: re-normalized `last` related lemmas' names. 04 December 2015, 09:21:55 UTC
1c4206c Pierre-Yves Strub 04 December 2015, 09:17:37 UTC Merge commit '987395315d36ddf36600d635513e295bf32d2422' into phl 04 December 2015, 09:17:37 UTC
b44ee94 Pierre-Yves Strub 03 December 2015, 16:50:12 UTC Refactoring more exn printers. 03 December 2015, 16:50:34 UTC
08e0fd4 Pierre-Yves Strub 03 December 2015, 16:50:02 UTC Do not select notations as operators. 03 December 2015, 16:50:33 UTC
9873953 Pierre-Yves Strub 03 December 2015, 16:50:12 UTC Refactoring more exn printers. 03 December 2015, 16:50:12 UTC
c9434a4 Pierre-Yves Strub 03 December 2015, 16:50:02 UTC Do not select notations as operators. 03 December 2015, 16:50:02 UTC
eca348a Pierre-Yves Strub 03 December 2015, 16:30:35 UTC Bind abbreviations in the env. 03 December 2015, 16:30:43 UTC
1535b3a Pierre-Yves Strub 03 December 2015, 16:30:35 UTC Bind abbreviations in the env. 03 December 2015, 16:30:35 UTC
e279c60 Pierre-Yves Strub 03 December 2015, 15:55:11 UTC Expressions are now printed using the formulas pp. 03 December 2015, 15:59:03 UTC
3f1d954 Pierre-Yves Strub 03 December 2015, 15:55:11 UTC Expressions are now printed using the formulas pp. 03 December 2015, 15:55:11 UTC
e1e1792 Pierre-Yves Strub 03 December 2015, 15:31:55 UTC `clear` now applies on axioms. Axioms are only cleared when proven via the cloning mechanism. 03 December 2015, 15:33:17 UTC
3c6d3bb Pierre-Yves Strub 03 December 2015, 15:29:42 UTC Fix printing of various hint databases. 03 December 2015, 15:33:16 UTC
57561d6 Pierre-Yves Strub 03 December 2015, 15:01:01 UTC Fix pruning of lemmas from various databases on th. closing. 03 December 2015, 15:33:13 UTC
9f44d3e Pierre-Yves Strub 03 December 2015, 15:31:55 UTC `clear` now applies on axioms. Axioms are only cleared when proven via the cloning mechanism. 03 December 2015, 15:31:55 UTC
9b64af4 Pierre-Yves Strub 03 December 2015, 15:29:42 UTC Fix printing of various hint databases. 03 December 2015, 15:29:42 UTC
bed175e Pierre-Yves Strub 03 December 2015, 15:01:01 UTC Fix pruning of lemmas from various databases on th. closing. 03 December 2015, 15:01:01 UTC
876b7ee Pierre-Yves Strub 03 December 2015, 14:27:58 UTC Push user error messages to a top-level module. This should allow using some hi-level modules in the pretty-printer module. 03 December 2015, 14:34:43 UTC
2ccfd90 Pierre-Yves Strub 03 December 2015, 14:34:36 UTC Fix compilation issues introduced by cherry-pick 000ed59. 03 December 2015, 14:34:42 UTC
9241f03 Pierre-Yves Strub 03 December 2015, 14:27:58 UTC Push user error messages to a top-level module. This should allow using some hi-level modules in the pretty-printer module. 03 December 2015, 14:27:58 UTC
62c3921 Benjamin Gregoire 03 December 2015, 10:17:27 UTC print type of added operators 03 December 2015, 11:41:44 UTC
b465dbe Benjamin Gregoire 03 December 2015, 10:17:27 UTC print type of added operators 03 December 2015, 10:17:27 UTC
4a454f3 Benjamin Gregoire 03 December 2015, 10:16:56 UTC add return type when printing operator 03 December 2015, 10:16:56 UTC
000ed59 Benjamin Gregoire 03 December 2015, 08:53:57 UTC allows underscore in pattern matching for fix point 03 December 2015, 09:00:35 UTC
4563255 Benjamin Gregoire 03 December 2015, 08:53:57 UTC allows underscore in pattern matching for fix point 03 December 2015, 08:58:44 UTC
a1d4e7c Pierre-Yves Strub 02 December 2015, 19:57:53 UTC `congr` handles goal of the form `P <=> Q` [fix #17275] 02 December 2015, 19:58:04 UTC
bd34470 Pierre-Yves Strub 02 December 2015, 19:57:53 UTC `congr` handles goal of the form `P <=> Q` [fix #17275] 02 December 2015, 19:57:53 UTC
e596e75 Pierre-Yves Strub 02 December 2015, 16:38:31 UTC PG keywords updated 02 December 2015, 16:38:31 UTC
c8346a6 Pierre-Yves Strub 02 December 2015, 16:36:54 UTC Type-checking of abbreviations. 02 December 2015, 16:38:15 UTC
8b7c8f3 Pierre-Yves Strub 02 December 2015, 16:38:05 UTC PG keywords updated 02 December 2015, 16:38:05 UTC
693c114 Pierre-Yves Strub 02 December 2015, 16:36:54 UTC Type-checking of abbreviations. 02 December 2015, 16:36:54 UTC
00c9f37 Pierre-Yves Strub 02 December 2015, 16:01:34 UTC Type checking of notations. 02 December 2015, 16:01:47 UTC
5710919 Pierre-Yves Strub 02 December 2015, 16:01:34 UTC Type checking of notations. 02 December 2015, 16:01:34 UTC
f290f1a Pierre-Yves Strub 02 December 2015, 13:49:45 UTC Simplify BG proof :) 02 December 2015, 13:50:08 UTC
9c9fe65 Pierre-Yves Strub 02 December 2015, 13:49:45 UTC Simplify BG proof :) 02 December 2015, 13:49:45 UTC
8200aec Benjamin Gregoire 02 December 2015, 13:31:37 UTC Add lemma mkseqP 02 December 2015, 13:45:05 UTC
ac800ec Pierre-Yves Strub 02 December 2015, 13:40:05 UTC Remove unusable /#= rw action + add /# as a i-p. 02 December 2015, 13:44:56 UTC
c1e46d7 Pierre-Yves Strub 02 December 2015, 13:40:05 UTC Remove unusable /#= rw action + add /# ats a i-p. 02 December 2015, 13:44:48 UTC
7ec2538 Benjamin Gregoire 02 December 2015, 13:31:37 UTC Add lemma mkseqP 02 December 2015, 13:31:56 UTC
6f2d37b Pierre-Yves Strub 02 December 2015, 11:50:03 UTC Parsing rules for notations/abbreviations. 02 December 2015, 11:50:12 UTC
16caef0 Pierre-Yves Strub 02 December 2015, 11:50:03 UTC Parsing rules for notations/abbreviations. 02 December 2015, 11:50:03 UTC
f97c4dd Pierre-Yves Strub 02 December 2015, 11:42:43 UTC Refactor parsing rules for operators decl/def. 02 December 2015, 11:43:56 UTC
d394f11 Pierre-Yves Strub 02 December 2015, 11:42:43 UTC Refactor parsing rules for operators decl/def. 02 December 2015, 11:43:07 UTC
2ba835a Pierre-Yves Strub 02 December 2015, 09:31:57 UTC README.md: update dependencies 02 December 2015, 11:19:22 UTC
91d4454 Benjamin Gregoire 02 December 2015, 11:14:08 UTC remove useless space in lemmas printing. 02 December 2015, 11:19:15 UTC
6cd962a Benjamin Gregoire 02 December 2015, 11:12:57 UTC fix bug in printing of abstract theory. 02 December 2015, 11:17:31 UTC
fabbf27 Pierre-Yves Strub 02 December 2015, 09:31:57 UTC README.md: update dependencies 02 December 2015, 11:16:02 UTC
c29fc84 Benjamin Gregoire 02 December 2015, 11:14:08 UTC remove useless space in lemmas printing. 02 December 2015, 11:14:36 UTC
4be5d7a Benjamin Gregoire 02 December 2015, 11:12:57 UTC fix bug in printing of abstract theory. 02 December 2015, 11:14:36 UTC
26ad56f Benjamin Gregoire 02 December 2015, 08:18:55 UTC improve PY proof script. 02 December 2015, 09:07:13 UTC
311ad83 Benjamin Gregoire 02 December 2015, 08:12:36 UTC fixing error message for typing of module expressions. 02 December 2015, 09:07:07 UTC
30389e6 Pierre-Yves Strub 02 December 2015, 08:41:19 UTC Refactor op-app destructor. 02 December 2015, 09:06:31 UTC
bba28f7 Pierre-Yves Strub 02 December 2015, 08:06:17 UTC Allow the use of `_` in tuple patterns. As in: `op ['a 'b] fst (x : 'a * 'b) = let (z, _) = x in x` 02 December 2015, 09:06:31 UTC
88b45b4 Pierre-Yves Strub 02 December 2015, 08:41:57 UTC Refactoring muhoare view implementation. 02 December 2015, 08:41:57 UTC
d0fa4cd Pierre-Yves Strub 02 December 2015, 08:41:19 UTC Refactor op-app destructor. 02 December 2015, 08:41:19 UTC
cbd608f Pierre-Yves Strub 02 December 2015, 08:06:17 UTC Allow the use of `_` in tuple patterns. As in: `op ['a 'b] fst (x : 'a * 'b) = let (z, _) = x in x` 02 December 2015, 08:22:51 UTC
99156b6 Benjamin Gregoire 02 December 2015, 08:18:55 UTC improve PY proof script. 02 December 2015, 08:18:55 UTC
0b16322 Benjamin Gregoire 02 December 2015, 08:12:36 UTC fixing error message for typing of module expressions. 02 December 2015, 08:13:27 UTC
7a77090 Pierre-Yves Strub 02 December 2015, 07:28:38 UTC Core fact about words. 02 December 2015, 07:28:46 UTC
e14c433 Pierre-Yves Strub 02 December 2015, 07:28:38 UTC Core fact about words. 02 December 2015, 07:28:38 UTC
90ece64 Benjamin Gregoire 01 December 2015, 21:45:59 UTC improve error messages for module application, and there localizations. 01 December 2015, 21:55:03 UTC
36ad55c Benjamin Gregoire 01 December 2015, 21:45:59 UTC improve error messages for module application, and there localizations. 01 December 2015, 21:51:05 UTC
cc67710 François Dupressoir 01 December 2015, 21:02:59 UTC Removing old quantifier negations from stdlib. 01 December 2015, 21:12:10 UTC
91a1969 François Dupressoir 01 December 2015, 20:51:59 UTC NewLogic: add lemmas for negation of existentials. This is so we can stop using 'the other ones'. 01 December 2015, 21:12:09 UTC
8f229a1 François Dupressoir 01 December 2015, 20:37:28 UTC Useful lemmas on random permutations. Needs cleaning up. 01 December 2015, 21:12:08 UTC
3915c77 François Dupressoir 01 December 2015, 20:10:09 UTC PRFs and PRP-PRF switching lemma. 01 December 2015, 21:12:07 UTC
1de78d7 François Dupressoir 01 December 2015, 15:06:29 UTC Fixing up new PRP libs and adding them back into the test suite. 01 December 2015, 21:12:06 UTC
c4da5f6 François Dupressoir 01 December 2015, 21:02:59 UTC Removing old quantifier negations from stdlib. 01 December 2015, 21:02:59 UTC
4a65689 François Dupressoir 01 December 2015, 20:51:59 UTC NewLogic: add lemmas for negation of existentials. This is so we can stop using 'the other ones'. 01 December 2015, 20:51:59 UTC
42a4a3b François Dupressoir 01 December 2015, 20:37:28 UTC Useful lemmas on random permutations. Needs cleaning up. 01 December 2015, 20:37:28 UTC
af346b2 François Dupressoir 01 December 2015, 20:10:09 UTC PRFs and PRP-PRF switching lemma. 01 December 2015, 20:16:02 UTC
9fe4d23 François Dupressoir 01 December 2015, 15:06:29 UTC Fixing up new PRP libs and adding them back into the test suite. 01 December 2015, 20:10:56 UTC
2998c27 Pierre-Yves Strub 01 December 2015, 17:10:55 UTC Hint database for auto-exact. Add a new hint mechanism for auto-applying lemmas. Lemmas are added to the auto base with: `hint exact : L1 ... Ln.` `trivial` (and all relatives) now tries to close any goal it is presented by applying one of the lemmas of the database --- closing any generated subgoal recursively. The lemmas in the hint database are not used when `trivial` tries to close the subgoals. Lemmas are applied using a rigid unification and with the view mechanism disabled. The current implementation is linear in the size of the database. A pre-selection mechanism may be necessary in case the hint database grows too much. 01 December 2015, 17:29:46 UTC
65eda54 Pierre-Yves Strub 01 December 2015, 17:10:55 UTC Hint database for auto-exact. Add a new hint mechanism for auto-applying lemmas. Lemmas are added to the auto base with: `hint exact : L1 ... Ln.` `trivial` (and all relatives) now tries to close any goal it is presented by applying one of the lemmas of the database --- closing any generated subgoal recursively. The lemmas in the hint database are not used when `trivial` tries to close the subgoals. Lemmas are applied using a rigid unification and with the view mechanism disabled. The current implementation is linear in the size of the database. A pre-selection mechanism may be necessary in case the hint database grows too much. 01 December 2015, 17:10:55 UTC
back to top