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 |
7cc81de | Pierre-Yves Strub | 01 December 2015, 15:29:19 UTC | .gitignore | 01 December 2015, 15:29:30 UTC |
e6a3241 | Pierre-Yves Strub | 01 December 2015, 15:29:19 UTC | .gitignore | 01 December 2015, 15:29:19 UTC |
e1b70b4 | Pierre-Yves Strub | 01 December 2015, 15:16:28 UTC | Pattern matching work modulo unfolding of locals. | 01 December 2015, 15:27:06 UTC |
214fcfc | Pierre-Yves Strub | 01 December 2015, 15:16:28 UTC | Pattern matching work modulo unfolding of locals. | 01 December 2015, 15:19:57 UTC |
1731c7e | Benjamin Gregoire | 01 December 2015, 14:55:01 UTC | improve error message: only monomorphic types are allowedt | 01 December 2015, 14:57:45 UTC |
a09868d | Benjamin Gregoire | 01 December 2015, 14:55:01 UTC | improve error message: only monomorphic types are allowed | 01 December 2015, 14:55:11 UTC |
ecaaf69 | Pierre-Yves Strub | 01 December 2015, 14:53:47 UTC | Exemplified new matching algo. | 01 December 2015, 14:54:52 UTC |
95a4b45 | Pierre-Yves Strub | 01 December 2015, 14:53:33 UTC | Better matching + matching always return a reduced subst. | 01 December 2015, 14:54:45 UTC |
6829f6b | Pierre-Yves Strub | 01 December 2015, 14:53:47 UTC | Exemplified new matching algo. | 01 December 2015, 14:53:47 UTC |
0db9002 | Pierre-Yves Strub | 01 December 2015, 14:53:33 UTC | Better matching + matching always return a reduced subst. | 01 December 2015, 14:53:33 UTC |
df925d2 | Pierre-Yves Strub | 01 December 2015, 13:31:21 UTC | In proof-term, arguments can be partially constructed. As in: `apply (foo (x + _))` | 01 December 2015, 13:31:40 UTC |
7143ede | Pierre-Yves Strub | 01 December 2015, 13:31:21 UTC | In proof-term, arguments can be partially constructed. As in: `apply (foo (x + _))` | 01 December 2015, 13:31:21 UTC |
0fcb523 | Pierre-Yves Strub | 01 December 2015, 12:03:49 UTC | algebra: do not use t_fail internally. | 01 December 2015, 12:03:59 UTC |
3e4e3d0 | Pierre-Yves Strub | 01 December 2015, 12:03:49 UTC | algebra: do not use t_fail internally. | 01 December 2015, 12:03:49 UTC |