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 |