| 7476fe1 | Pierre-Yves Strub | 14 December 2015, 12:02:17 UTC | Removing internal implem. of removed `move=> x!` | 14 December 2015, 12:02:26 UTC |
| 65f95ac | Pierre-Yves Strub | 14 December 2015, 11:58:56 UTC | Intro-pattern: `n!->` (n optional, `->` can be `<-`) Repeat `->` at most `n` times. | 14 December 2015, 11:59:14 UTC |
| 108a489 | Pierre-Yves Strub | 14 December 2015, 11:58:14 UTC | Removing (from parser) intro-patterm `x!` (unused) | 14 December 2015, 11:59:14 UTC |
| f61598c | Pierre-Yves Strub | 14 December 2015, 11:38:27 UTC | Lexems `<-`, `->`, `<<-`, `->>` can now be glued together. | 14 December 2015, 11:38:46 UTC |
| 53b710e | François Dupressoir | 14 December 2015, 10:21:09 UTC | Predicates on relations from SSR. transpose should be made a parse-only notation | 14 December 2015, 11:38:45 UTC |
| 49d4ab8 | Pierre-Yves Strub | 14 December 2015, 10:13:15 UTC | Lists: subseq + more on sorts. Some admits in subseq. | 14 December 2015, 10:13:47 UTC |
| 3aa90e0 | Benjamin Gregoire | 14 December 2015, 04:36:01 UTC | generalize lemma | 14 December 2015, 10:13:46 UTC |
| b690a3b | Pierre-Yves Strub | 13 December 2015, 19:18:39 UTC | IntDiv: nits. | 13 December 2015, 19:19:00 UTC |
| 1e48f0a | Pierre-Yves Strub | 13 December 2015, 14:15:49 UTC | New intro-pattern: `<*>` This intro-pattern applies `subst` on all the top-assumptions. It is possible to restrict the construct to exactly `n` top-assumptions by rewriting `n!<*>`. Top-assumptions that have been substituted are cleared, other ones are kept untouched. | 13 December 2015, 14:16:19 UTC |
| b7ffa02 | Pierre-Yves Strub | 13 December 2015, 14:14:31 UTC | Syntax change: `[n*]` -> `[n!*]` | 13 December 2015, 14:16:18 UTC |
| 4388214 | Pierre-Yves Strub | 12 December 2015, 19:59:46 UTC | I-p `[*]` can now do case analysis of ind. pred. ~ to `and`. Syntax is `[~*]`. The full syntax of this i-p is now: `move=> [int?~?/?*]` | 12 December 2015, 20:03:33 UTC |
| c09a98a | Pierre-Yves Strub | 12 December 2015, 11:55:01 UTC | I-p `[*]` can now delta-unfold on demande. The syntax is `[/*]`. The full syntax of this intro-pattern is now: `move=> [int?/?*]` | 12 December 2015, 11:55:17 UTC |
| 49ccbc4 | Pierre-Yves Strub | 12 December 2015, 11:41:41 UTC | Intro-pattern `[!*]`. Same as `[*]`, but destruct all top-assumptions. | 12 December 2015, 11:55:16 UTC |
| 95d9ef9 | Pierre-Yves Strub | 12 December 2015, 11:22:35 UTC | Intro-pattern `[*]` do not delta-unfold top-assumptions. | 12 December 2015, 11:55:14 UTC |
| 2763987 | Pierre-Yves Strub | 12 December 2015, 10:38:11 UTC | Intro-pattern `[*]` fully destruct all the top-ands of the top-assumption. The variant `[n*]` do the same-process on the `n` first top-assumptions. | 12 December 2015, 10:38:44 UTC |
| e188bb2 | Pierre-Yves Strub | 11 December 2015, 19:29:49 UTC | t_left -> t_right. | 11 December 2015, 19:30:09 UTC |
| 055f122 | Pierre-Yves Strub | 11 December 2015, 18:17:46 UTC | `left` / `right` now handles ind. pred. ~ to or. | 11 December 2015, 18:18:17 UTC |
| a8d79e1 | Pierre-Yves Strub | 11 December 2015, 16:56:55 UTC | `split` now handles ind. pred. ~ to and. | 11 December 2015, 18:18:16 UTC |
| c37c760 | Pierre-Yves Strub | 11 December 2015, 16:37:25 UTC | Check for duplicated constructor names in ind. pred. | 11 December 2015, 18:18:15 UTC |
| a53f58b | Pierre-Yves Strub | 11 December 2015, 16:37:15 UTC | Ind. pr. intro lemmas have the name of their respective ctr. | 11 December 2015, 18:18:14 UTC |
| 2cccc61 | Pierre-Yves Strub | 11 December 2015, 16:18:49 UTC | `case` tactic now works on inductive predicates. | 11 December 2015, 18:18:13 UTC |
| a9c3b6b | François Dupressoir | 11 December 2015, 14:43:03 UTC | PRP<->PRF-like lemma when the adversary can query the inverse permutation oracle. | 11 December 2015, 14:46:45 UTC |
| cc8ba00 | Pierre-Yves Strub | 11 December 2015, 14:38:31 UTC | Do not use `felsum` op. anymore. | 11 December 2015, 14:39:15 UTC |
| 6154aaa | Pierre-Yves Strub | 11 December 2015, 14:10:44 UTC | Ind. predicate are now equipped with their intro/elim schemes. | 11 December 2015, 14:10:53 UTC |
| 2a41e40 | Pierre-Yves Strub | 11 December 2015, 14:08:37 UTC | In BitWord, inline `card` (with 2) | 11 December 2015, 14:09:05 UTC |
| 6440e8d | Benjamin Gregoire | 11 December 2015, 13:48:54 UTC | add trivial lemma | 11 December 2015, 14:09:04 UTC |
| fc23436 | Benjamin Gregoire | 11 December 2015, 10:43:48 UTC | improve lemma rng_set | 11 December 2015, 12:00:26 UTC |
| 96ce566 | Pierre-Yves Strub | 11 December 2015, 11:56:16 UTC | Inductive (non-rec) pred. parsing + typing. | 11 December 2015, 11:59:59 UTC |
| f95613d | Pierre-Yves Strub | 11 December 2015, 10:34:27 UTC | Factorize out predicates related typing functions. | 11 December 2015, 11:56:34 UTC |
| a09fa95 | Benjamin Gregoire | 10 December 2015, 07:38:55 UTC | add lemmas | 11 December 2015, 09:51:20 UTC |
| 405f7dd | Pierre-Yves Strub | 10 December 2015, 15:17:02 UTC | Do not complain about goal count mismatch on `[]`. | 10 December 2015, 15:17:13 UTC |
| b3066c4 | Pierre-Yves Strub | 10 December 2015, 15:05:46 UTC | `case` && `elim` now takes clear genpattern + views (for `case`). | 10 December 2015, 15:05:56 UTC |
| cdb1f75 | Pierre-Yves Strub | 10 December 2015, 13:03:44 UTC | Remove duplicated abbrev. for (-) in RealOrder. | 10 December 2015, 13:03:49 UTC |
| 13b6eeb | Pierre-Yves Strub | 10 December 2015, 12:16:06 UTC | PG: new var.: easycrypt-prog-args | 10 December 2015, 12:16:13 UTC |
| bddc0d5 | Pierre-Yves Strub | 10 December 2015, 08:50:50 UTC | Categorize `rewrite` as a case-like tactic. This means that if the first i-p (pruning simplication ones) is a `case` i-p, no case analysis is done. Previous behaviour can be recovered by prepending a `-` (i.e. by flusing the i-p chain) Scripts can be updated with: gsed -i 's@rewrite\([^;]*=>\( */=\)\?\) *\[@rewrite\1 -[@g' **/*.ec* | 10 December 2015, 09:21:58 UTC |
| a820b13 | Pierre-Yves Strub | 10 December 2015, 08:25:10 UTC | Remove `intro` Scripts can be updated with: gsed -i 's/intros *\(=>\)\? */move=> /g' **/*.ec* | 10 December 2015, 09:21:50 UTC |
| 243c3ba | Pierre-Yves Strub | 10 December 2015, 08:53:08 UTC | Remove `generalize` Scripts should now use `move: `. Use `gsed -i 's/generalize */move: /g' **/*.ec*` to update scripts. | 10 December 2015, 09:21:41 UTC |
| 1e62fd9 | Pierre-Yves Strub | 10 December 2015, 09:17:45 UTC | In stdlib, don't assume that rewrite in a non-case tactic. | 10 December 2015, 09:21:32 UTC |
| 2fed99d | Pierre-Yves Strub | 10 December 2015, 09:17:23 UTC | In stdlib, don't use `intros` anymore | 10 December 2015, 09:20:33 UTC |
| 9f8880d | Pierre-Yves Strub | 10 December 2015, 08:45:38 UTC | In stdlib, don't use `generalize` anymore | 10 December 2015, 09:20:24 UTC |
| 6937ece | Pierre-Yves Strub | 09 December 2015, 19:29:50 UTC | In pp: priority of uniry arith ops. have a priority equal to their binary counter-parts. This is in accordance with the parser definition. As a consequence, when mixing [-]/[+] with (-)/(+), the pp now prints explicit parentheses in all cases. Given the unusual precedences unary operators have, we should stick to this until we fix them. | 09 December 2015, 19:30:13 UTC |
| 92900c9 | Pierre-Yves Strub | 09 December 2015, 16:46:57 UTC | Crude detection of identity rewriting. The mechanism is to forbid non-keyed matching in `rewrite` when LHS && RHS of the rewriting equation are convertible. Currently, the whole `rewrite` is rejected if the matching succeeds but the result would result in a identity rewriting. A better mechanism should embed the identity detection rewriting mechanism into the form matching one. | 09 December 2015, 16:49:49 UTC |
| b3f11a9 | Pierre-Yves Strub | 09 December 2015, 15:50:59 UTC | Add 'eta-reduction'. | 09 December 2015, 15:51:09 UTC |
| 0fa2523 | Pierre-Yves Strub | 09 December 2015, 15:33:56 UTC | Fix pretty-printer w.r.t. operators' priorities. [fix #17276] | 09 December 2015, 15:34:08 UTC |
| 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 |
