03fd7f2 | Pierre-Yves Strub | 10 October 2017, 09:04:16 UTC | compile with up-to-date toolchain | 10 October 2017, 09:04:16 UTC |
9f6a2f9 | Benjamin Gregoire | 07 July 2016, 06:32:45 UTC | add make | 07 July 2016, 06:32:45 UTC |
776af38 | Pierre-Yves Strub | 02 April 2016, 08:09:32 UTC | Why3: => 0.87 | 06 July 2016, 20:52:42 UTC |
f3ba127 | Pierre-Yves Strub | 12 January 2016, 09:43:08 UTC | Better parsing of mdistr types. | 12 January 2016, 09:43:08 UTC |
f007c3f | Pierre-Yves Strub | 10 January 2016, 11:49:40 UTC | Nits in IntDiv. | 10 January 2016, 11:50:00 UTC |
d42f414 | François Dupressoir | 08 January 2016, 19:26:29 UTC | Uniform distribution on words: Splitting uniformity and fullness. | 08 January 2016, 20:22:16 UTC |
0f42e50 | Benjamin Gregoire | 08 January 2016, 09:31:16 UTC | small fix | 08 January 2016, 12:04:40 UTC |
f026337 | François Dupressoir | 08 January 2016, 03:48:49 UTC | Uniform distributions are uniform. | 08 January 2016, 03:49:29 UTC |
da610f0 | Pierre-Yves Strub | 08 January 2016, 03:46:28 UTC | do not remove whitespaces (.dir-locals) - PG mode is buggy on that | 08 January 2016, 03:46:38 UTC |
fbd222b | Pierre-Yves Strub | 05 January 2016, 15:51:48 UTC | Refactoring a bit Vagrantfile. | 05 January 2016, 21:59:08 UTC |
352f5cc | Pierre-Yves Strub | 04 January 2016, 14:57:38 UTC | remove trailing whitespaces | 04 January 2016, 14:57:38 UTC |
00622b9 | Pierre-Yves Strub | 04 January 2016, 14:55:43 UTC | emacs local variables for trailing whitespaces removal. | 04 January 2016, 14:57:20 UTC |
8ae369b | Pierre-Yves Strub | 04 January 2016, 14:33:06 UTC | license: do not create trailing whitespaces | 04 January 2016, 14:57:12 UTC |
675c6bd | Benjamin Gregoire | 04 January 2016, 12:56:17 UTC | small improvement | 04 January 2016, 14:26:55 UTC |
1d1f362 | Pierre-Yves Strub | 03 January 2016, 10:13:41 UTC | COPYRIGHT (2016 / headers) | 03 January 2016, 10:13:41 UTC |
6b8e0e2 | Pierre-Yves Strub | 03 January 2016, 10:13:19 UTC | COPYRIGHT (2016) | 03 January 2016, 10:13:19 UTC |
8133719 | Pierre-Yves Strub | 22 December 2015, 20:02:43 UTC | Variant of `case` that retains the case equation. Syntax is `case _: ...`, and work as in vanilla variant, but retains the case equation (that is pushed as a top-assumption). | 03 January 2016, 10:12:30 UTC |
0e9c8b6 | Benjamin Gregoire | 18 December 2015, 18:27:59 UTC | replug + generalize the tactic exists* to any expression. | 03 January 2016, 10:10:03 UTC |
0546b4a | Benjamin Gregoire | 18 December 2015, 14:58:26 UTC | minor changes | 18 December 2015, 20:59:41 UTC |
0bf18f8 | Benjamin Gregoire | 18 December 2015, 14:54:15 UTC | minor changes. | 18 December 2015, 20:59:40 UTC |
0b95d24 | François Dupressoir | 18 December 2015, 09:18:40 UTC | NewDistr: extending standard distributions with support lemmas. | 18 December 2015, 20:59:40 UTC |
7c79378 | Pierre-Yves Strub | 18 December 2015, 20:59:28 UTC | PG keywords updated | 18 December 2015, 20:59:28 UTC |
f0d849f | Benjamin Gregoire | 18 December 2015, 07:53:04 UTC | add lemmas in the sodlib | 18 December 2015, 08:13:07 UTC |
98986d8 | Benjamin Gregoire | 17 December 2015, 21:21:10 UTC | add more possibilities to change the bound in phoare | 18 December 2015, 08:13:06 UTC |
06d13a5 | Pierre-Yves Strub | 17 December 2015, 21:03:44 UTC | Nits in Lists (cleaning a bit + some basic results) | 17 December 2015, 21:04:13 UTC |
4ea99e2 | Pierre-Yves Strub | 17 December 2015, 20:26:15 UTC | remove some debugging printf | 17 December 2015, 20:26:15 UTC |
51c94f5 | Benjamin Gregoire | 17 December 2015, 17:04:26 UTC | print the goal by default in error message for apply + small modification of the formatting | 17 December 2015, 19:55:01 UTC |
b784ecd | Pierre-Yves Strub | 17 December 2015, 16:17:44 UTC | In `phl` tactics, display the goal when an internal `apply` failed. | 17 December 2015, 16:18:01 UTC |
7f2bfa9 | Benjamin Gregoire | 17 December 2015, 15:56:36 UTC | Move HiGoal.LowApply to LowGoal.Apply + make use of the hi/low-apply in phl tactics | 17 December 2015, 16:10:56 UTC |
ddd9e62 | Benjamin Gregoire | 17 December 2015, 15:56:03 UTC | one more time Francois ... | 17 December 2015, 15:57:36 UTC |
c95a61f | Pierre-Yves Strub | 16 December 2015, 18:31:07 UTC | Start playing a bit with `hint exact` in the stdlib. | 16 December 2015, 18:31:22 UTC |
062d0f8 | Pierre-Yves Strub | 16 December 2015, 18:30:53 UTC | `exact` hints can be declared local. Such hints are not imported. | 16 December 2015, 18:31:21 UTC |
28d74f3 | Pierre-Yves Strub | 16 December 2015, 18:14:40 UTC | Code style (.ec) | 16 December 2015, 18:31:19 UTC |
8ab78bb | Pierre-Yves Strub | 16 December 2015, 18:09:55 UTC | Fix `[*]` i-p that was doing some delta. | 16 December 2015, 18:10:20 UTC |
04743fa | François Dupressoir | 16 December 2015, 18:07:14 UTC | Fold version of oracle looping. | 16 December 2015, 18:10:19 UTC |
f4b94e8 | Pierre-Yves Strub | 16 December 2015, 18:06:01 UTC | Implement ssr compatible naming for i-p. - `move=> _` does a late clear - `move=> ?` does an anonymous (_) intro This is currently not enabled by default. The option `oldip` has first to be cleared (`pragma -oldip`) | 16 December 2015, 18:07:43 UTC |
65269da | Pierre-Yves Strub | 16 December 2015, 17:25:43 UTC | Internals: ax_spec is no more a `form option` | 16 December 2015, 17:25:53 UTC |
d378204 | François Dupressoir | 16 December 2015, 17:09:17 UTC | Some cleaning on IterProc. | 16 December 2015, 17:10:37 UTC |
a722c7a | Pierre-Yves Strub | 16 December 2015, 16:17:34 UTC | ambient `auto`: do not fail on first non-applicable lemma in the db. Really... | 16 December 2015, 16:17:42 UTC |
62ee9c8 | Pierre-Yves Strub | 16 December 2015, 16:02:28 UTC | ambient `auto`: do not fail on first non-applicable lemma in the db. | 16 December 2015, 16:02:36 UTC |
46901a7 | Pierre-Yves Strub | 16 December 2015, 15:31:27 UTC | New syntax for equiv. eq: `={| f1, ..., fn |}`. This syntax is a notation for `f1{1} = f1{2} /\ ...` [close #17284] | 16 December 2015, 15:31:38 UTC |
0b4bb01 | Pierre-Yves Strub | 16 December 2015, 12:00:28 UTC | Refactor theory replay in its own module. | 16 December 2015, 12:00:36 UTC |
8f6c385 | Pierre-Yves Strub | 16 December 2015, 10:02:40 UTC | Refactoring hi-cloning into smaller functions. | 16 December 2015, 10:06:49 UTC |
62ee2cc | Pierre-Yves Strub | 15 December 2015, 14:29:55 UTC | Refactoring .mli | 15 December 2015, 14:30:07 UTC |
b20b595 | Benjamin Gregoire | 15 December 2015, 11:50:24 UTC | set default value max_lemmas to 0 when wanted_lemmas is given | 15 December 2015, 12:43:27 UTC |
18353b9 | Pierre-Yves Strub | 15 December 2015, 11:39:50 UTC | A bit more on chunking. | 15 December 2015, 11:40:22 UTC |
3262b68 | François Dupressoir | 15 December 2015, 10:50:12 UTC | Generic reasoning about procedure iteration. | 15 December 2015, 11:40:21 UTC |
6065048 | François Dupressoir | 15 December 2015, 10:11:04 UTC | Making transpose an abbreviation. Also reworking a proof in Rel to make it fit in 80 chars. | 15 December 2015, 11:40:20 UTC |
7c1e7b7 | Pierre-Yves Strub | 15 December 2015, 08:40:11 UTC | Parse only notations. Notation can be declared parse-only via the option `printing`, as in: `abbrev [-printing] succ (x : int) = x` [close #17280] | 15 December 2015, 08:45:06 UTC |
b02e4e4 | Pierre-Yves Strub | 15 December 2015, 08:30:18 UTC | Factor out notations typing. | 15 December 2015, 08:45:06 UTC |
f83acc1 | Benjamin Gregoire | 15 December 2015, 07:43:16 UTC | improve eager: eager proc works on abstract functions. | 15 December 2015, 08:45:05 UTC |
75174e7 | Benjamin Gregoire | 14 December 2015, 22:58:59 UTC | generalize lemma ... | 15 December 2015, 07:09:38 UTC |
0901c4f | Pierre-Yves Strub | 14 December 2015, 19:40:16 UTC | New occurence selector: `{+}`. Select all occurences. Allow to not clear generalized variables, using: `move: {+}x` (~ to `move: (x)`). | 14 December 2015, 19:43:55 UTC |
f65f5f1 | Pierre-Yves Strub | 14 December 2015, 17:00:47 UTC | Post-tactic generalize. Syntax is `tactic <@ foo`. Can be mixed with `tactic=> ...`. | 14 December 2015, 17:07:28 UTC |
06a078f | Pierre-Yves Strub | 14 December 2015, 16:03:29 UTC | Allows chaining '=> ...' Subsequent `=> ...` do not perform a case-analysis by default. | 14 December 2015, 16:05:19 UTC |
55a997a | Pierre-Yves Strub | 14 December 2015, 15:26:02 UTC | Simplification i-p/rw that do not break the product compatibility. Syntax is `/~=` && `//~=` (with done) | 14 December 2015, 15:26:36 UTC |
58337f0 | Pierre-Yves Strub | 14 December 2015, 14:21:43 UTC | Do not clear local hyps when generalized as-is. | 14 December 2015, 14:23:31 UTC |
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 |