| 666c7c6 | François Dupressoir | 25 January 2016, 21:04:56 UTC | Modernizing Drestrict and Dexcepted. Updating standard lib. We still need to make sure that Distr.Drestr and Distr.Dexcepted are not used anywhere else. Then burn them down and dance on their ashes. | 25 January 2016, 21:04:56 UTC |
| 11d8d1b | François Dupressoir | 25 January 2016, 16:53:36 UTC | NewDistr product distribution: a first stab. Holes to be filled in regarding sums over lists of pairs. A note worthy of discussion and changes if one thinks them necessary. And somthing to do before the old Pair.Dprod can be swapped out entirely. | 25 January 2016, 16:53:36 UTC |
| c0b807b | Pierre-Yves Strub | 25 January 2016, 11:57:21 UTC | `crush` now ends with a goal simplification. | 25 January 2016, 11:57:21 UTC |
| 682eacf | Pierre-Yves Strub | 25 January 2016, 11:51:21 UTC | In `|>` & `/>`, only rewrite hypotheses using alpha-conv. | 25 January 2016, 11:51:21 UTC |
| 22824dd | Pierre-Yves Strub | 25 January 2016, 11:39:53 UTC | Enhance hyps. conversion. | 25 January 2016, 11:39:53 UTC |
| 22e81c4 | Pierre-Yves Strub | 25 January 2016, 10:31:10 UTC | New distr: biased coins. | 25 January 2016, 10:31:10 UTC |
| b7be81c | Pierre-Yves Strub | 23 January 2016, 20:59:25 UTC | Fix MEE-CBC (weak-check) | 23 January 2016, 20:59:25 UTC |
| 33fe060 | Pierre-Yves Strub | 23 January 2016, 20:59:05 UTC | Add a test-config entry for MEE-CBC. | 23 January 2016, 20:59:05 UTC |
| 8430fab | François Dupressoir | 23 January 2016, 12:45:13 UTC | Aftermath of fixes in Number. | 23 January 2016, 12:45:13 UTC |
| 06952da | François Dupressoir | 23 January 2016, 11:49:25 UTC | Fix the Numbers fix. | 23 January 2016, 11:49:25 UTC |
| 8dd0763 | Pierre-Yves Strub | 22 January 2016, 20:20:38 UTC | some fix in Numbers | 22 January 2016, 20:20:38 UTC |
| a9eab14 | Pierre-Yves Strub | 22 January 2016, 14:19:14 UTC | module namespace can now be prefixed by Top/Self. [fix #17294] | 22 January 2016, 14:19:14 UTC |
| 9a70f94 | Pierre-Yves Strub | 22 January 2016, 13:51:31 UTC | Tweaking reals simplification | 22 January 2016, 13:51:31 UTC |
| dcb60df | Pierre-Yves Strub | 22 January 2016, 11:40:00 UTC | Fix various bugs in real simplification. [fix #17293] | 22 January 2016, 11:40:27 UTC |
| c96ffdb | François Dupressoir | 22 January 2016, 11:38:41 UTC | A quick cleanup of one example. Highlights some missing things in real summability. | 22 January 2016, 11:38:41 UTC |
| 9633859 | François Dupressoir | 22 January 2016, 10:18:36 UTC | Adding lemmas on injectivity of rcons. | 22 January 2016, 10:18:36 UTC |
| 5dac0f2 | François Dupressoir | 22 January 2016, 10:17:38 UTC | Adding some support lemmas to NewLogic. Plus some cleanup. | 22 January 2016, 10:17:38 UTC |
| dda4828 | Pierre-Yves Strub | 21 January 2016, 17:43:53 UTC | `progress*`-like intro-pattern. `move=> |>` does a `progress` like job, but merges all the generated subgoals as their conjunction. `move=> />` does the same, but up to delta-conversion. | 21 January 2016, 17:43:53 UTC |
| 30dfd89 | Pierre-Yves Strub | 21 January 2016, 14:17:17 UTC | Fixing stdlib w.r.t recent changes | 21 January 2016, 14:17:53 UTC |
| a2baa23 | Pierre-Yves Strub | 21 January 2016, 14:04:41 UTC | New intro-pattern: + `move=> n?` is equivalent to `move=> ?` n times + `move=> *` is equivalent to `move=> ?` as much as possible. | 21 January 2016, 14:17:53 UTC |
| 4114134 | Pierre-Yves Strub | 21 January 2016, 11:37:59 UTC | Allow i-p: `n!->>` & syntax change for `n!->`. | 21 January 2016, 14:17:53 UTC |
| f4831e6 | Pierre-Yves Strub | 21 January 2016, 11:07:03 UTC | In newip, change name generation of anonymous variables. | 21 January 2016, 14:05:29 UTC |
| 9053345 | Pierre-Yves Strub | 21 January 2016, 09:54:48 UTC | Tacticals now support to be decorated with intro-patterns. | 21 January 2016, 14:05:29 UTC |
| 741c5fc | Pierre-Yves Strub | 21 January 2016, 09:31:08 UTC | Reduce `e1 = e2` to `true` when e1 ~ e2 | 21 January 2016, 14:05:29 UTC |
| 469d7c5 | François Dupressoir | 21 January 2016, 13:25:32 UTC | Base lemmas regarding b2r. | 21 January 2016, 13:25:32 UTC |
| 8e1a8de | François Dupressoir | 21 January 2016, 09:23:02 UTC | Fixing a RealSeq proof. | 21 January 2016, 09:23:02 UTC |
| a9cefc6 | François Dupressoir | 21 January 2016, 09:17:52 UTC | Starting set of theories on query counting. | 21 January 2016, 09:17:52 UTC |
| 66f9db6 | François Dupressoir | 21 January 2016, 09:17:23 UTC | Rename Hybrid PKE theory to avoid clash. | 21 January 2016, 09:17:32 UTC |
| 2ecf68b | Pierre-Yves Strub | 20 January 2016, 15:59:15 UTC | i-p/r-w: //# (= // + /#) | 20 January 2016, 15:59:20 UTC |
| 0acdd55 | Benjamin Gregoire | 20 January 2016, 15:55:18 UTC | adding lemma on image(map) | 20 January 2016, 15:55:18 UTC |
| 2141c88 | Benjamin Gregoire | 19 January 2016, 13:17:12 UTC | give a definition to real absolute value | 19 January 2016, 13:22:12 UTC |
| 1ac65a5 | Pierre-Yves Strub | 19 January 2016, 13:20:27 UTC | Top-module `datatypes` (export option/pair/int/real) | 19 January 2016, 13:20:27 UTC |
| ccb964d | Pierre-Yves Strub | 19 January 2016, 12:19:08 UTC | purge reals from old axioms + update stdlib | 19 January 2016, 12:19:08 UTC |
| 27a512d | Benjamin Gregoire | 19 January 2016, 09:30:57 UTC | improve translation for real | 19 January 2016, 09:31:05 UTC |
| 76e2223 | Pierre-Yves Strub | 18 January 2016, 13:56:21 UTC | Add an implementation of EcBigInt based on OCaml Big_int. | 18 January 2016, 13:57:09 UTC |
| ca1d156 | Pierre-Yves Strub | 18 January 2016, 13:55:40 UTC | Fix: use EcBigInt comparison, not pervasive one. | 18 January 2016, 13:56:49 UTC |
| d7e8efd | Pierre-Yves Strub | 18 January 2016, 09:42:30 UTC | Change syntax for inductive predicates: `inductive ... := |? C of ... | D of ...` or `inductive ... := [ C of ... | D of ... ]` | 18 January 2016, 09:46:52 UTC |
| 4335564 | François Dupressoir | 15 January 2016, 14:10:10 UTC | Removing some unstable smt calls. | 15 January 2016, 14:14:24 UTC |
| accf29d | François Dupressoir | 15 January 2016, 14:03:05 UTC | Pushing Dbool out. Weak-Check works. | 15 January 2016, 14:14:24 UTC |
| 2026adf | Pierre-Yves Strub | 15 January 2016, 13:50:48 UTC | PRG examples go though again. | 15 January 2016, 13:50:48 UTC |
| 28bf034 | François Dupressoir | 15 January 2016, 09:55:23 UTC | Getting started on updating the PRG proof. | 15 January 2016, 09:55:23 UTC |
| 1cf7b01 | Pierre-Yves Strub | 10 January 2016, 11:49:40 UTC | Nits in IntDiv. | 10 January 2016, 11:49:40 UTC |
| 0440bb1 | François Dupressoir | 08 January 2016, 19:26:29 UTC | Uniform distribution on words: Splitting uniformity and fullness. | 08 January 2016, 19:26:39 UTC |
| b66aa85 | François Dupressoir | 08 January 2016, 03:48:49 UTC | Uniform distributions are uniform. | 08 January 2016, 03:48:56 UTC |
| d945d87 | 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:28 UTC |
| a9b7ed4 | Pierre-Yves Strub | 05 January 2016, 15:51:48 UTC | Refactoring a bit Vagrantfile. | 05 January 2016, 15:51:48 UTC |
| 537c4f5 | Pierre-Yves Strub | 04 January 2016, 14:55:18 UTC | remove trailing whitespaces | 04 January 2016, 14:56:32 UTC |
| fee4b48 | Pierre-Yves Strub | 04 January 2016, 14:55:43 UTC | emacs local variables for trailing whitespaces removal. | 04 January 2016, 14:56:18 UTC |
| 8768fc3 | Pierre-Yves Strub | 04 January 2016, 14:33:06 UTC | license: do not create trailing whitespaces | 04 January 2016, 14:33:06 UTC |
| 27a6617 | Benjamin Gregoire | 04 January 2016, 12:56:17 UTC | small improvement | 04 January 2016, 12:56:38 UTC |
| 17cc307 | Pierre-Yves Strub | 03 January 2016, 10:14:14 UTC | COPYRIGHT (2016 / headers) | 03 January 2016, 10:14:14 UTC |
| b7b3f0a | Pierre-Yves Strub | 03 January 2016, 10:13:19 UTC | COPYRIGHT (2016) | 03 January 2016, 10:14:08 UTC |
| 6b35ced | 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). | 22 December 2015, 20:18:35 UTC |
| a4c1ff3 | Benjamin Gregoire | 18 December 2015, 18:27:59 UTC | generalize the tactic exists * to any expression not only to variables or memory space (glob) | 18 December 2015, 18:28:12 UTC |
| d7b2a8e | Benjamin Gregoire | 18 December 2015, 14:58:26 UTC | minor changes | 18 December 2015, 18:28:12 UTC |
| 493d803 | Benjamin Gregoire | 18 December 2015, 14:54:15 UTC | minor changes. | 18 December 2015, 18:28:12 UTC |
| 66b2fd0 | François Dupressoir | 18 December 2015, 09:18:40 UTC | NewDistr: extending standard distributions with support lemmas. | 18 December 2015, 09:19:02 UTC |
| be94b0e | François Dupressoir | 17 December 2015, 17:07:29 UTC | Keywords | 18 December 2015, 09:19:02 UTC |
| 48e83b8 | Benjamin Gregoire | 18 December 2015, 07:53:04 UTC | add lemmas in the sodlib | 18 December 2015, 07:53:04 UTC |
| 8ef94a1 | Benjamin Gregoire | 17 December 2015, 21:21:10 UTC | add more possibilities to change the bound in phoare | 17 December 2015, 21:21:20 UTC |
| 7e0f413 | Pierre-Yves Strub | 17 December 2015, 21:03:44 UTC | Nits in Lists (cleaning a bit + some basic results) | 17 December 2015, 21:03:44 UTC |
| 9e4450f | Pierre-Yves Strub | 17 December 2015, 20:26:15 UTC | remove some debugging printf | 17 December 2015, 20:26:23 UTC |
| bedebc1 | 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, 17:04:26 UTC |
| 84ddbac | 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:17:44 UTC |
| 6997f1a | 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:31 UTC |
| 51c5713 | Benjamin Gregoire | 17 December 2015, 15:56:03 UTC | one more time Francois ... | 17 December 2015, 15:56:59 UTC |
| f359016 | 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:07 UTC |
| 0ff7403 | 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:30:53 UTC |
| d23b15d | Pierre-Yves Strub | 16 December 2015, 18:14:40 UTC | Code style (.ec) | 16 December 2015, 18:14:40 UTC |
| c29081d | Pierre-Yves Strub | 16 December 2015, 18:09:55 UTC | Fix `[*]` i-p that was doing some delta. | 16 December 2015, 18:10:08 UTC |
| a4f23ad | François Dupressoir | 16 December 2015, 18:07:14 UTC | Fold version of oracle looping. | 16 December 2015, 18:07:31 UTC |
| e873310 | 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:06:01 UTC |
| 51b29d2 | Pierre-Yves Strub | 16 December 2015, 17:25:43 UTC | Internals: ax_spec is no more a `form option` | 16 December 2015, 17:25:43 UTC |
| c50c1a1 | François Dupressoir | 16 December 2015, 17:09:17 UTC | Some cleaning on IterProc. | 16 December 2015, 17:09:31 UTC |
| 00049f2 | 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:34 UTC |
| 462ae7a | 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:28 UTC |
| 3547feb | 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:27 UTC |
| f47a90d | Pierre-Yves Strub | 16 December 2015, 12:00:28 UTC | Refactor theory replay in its own module. | 16 December 2015, 12:00:28 UTC |
| c4250b0 | Pierre-Yves Strub | 16 December 2015, 10:02:40 UTC | Refactoring hi-cloning into smaller functions. | 16 December 2015, 10:03:02 UTC |
| a0fdb87 | Pierre-Yves Strub | 15 December 2015, 14:29:55 UTC | Refactoring .mli | 15 December 2015, 14:29:55 UTC |
| 82894f3 | Benjamin Gregoire | 15 December 2015, 11:50:24 UTC | set default value max_lemmas to 0 when wanted_lemmas is given | 15 December 2015, 11:50:32 UTC |
| c0c489b | Pierre-Yves Strub | 15 December 2015, 11:39:50 UTC | A bit more on chunking. | 15 December 2015, 11:40:02 UTC |
| 084bf55 | François Dupressoir | 15 December 2015, 10:50:12 UTC | Generic reasoning about procedure iteration. | 15 December 2015, 10:50:12 UTC |
| 723525b | 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, 10:11:04 UTC |
| dce8518 | 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:41:40 UTC |
| 6f73974 | Pierre-Yves Strub | 15 December 2015, 08:30:18 UTC | Factor out notations typing. | 15 December 2015, 08:41:40 UTC |
| 7974eca | Benjamin Gregoire | 15 December 2015, 07:43:16 UTC | improve eager: eager proc works on abstract functions. | 15 December 2015, 07:43:16 UTC |
| 8bb1ad7 | Benjamin Gregoire | 14 December 2015, 22:58:59 UTC | generalize lemma ... | 14 December 2015, 22:59:07 UTC |
| 50c77ff | 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:40:28 UTC |
| 4e71af7 | 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:10:26 UTC |
| c359be3 | Pierre-Yves Strub | 14 December 2015, 16:03:29 UTC | Allows chaining '=> ...' Subsequence `=> ...` do not perform a case-analysis by default. | 14 December 2015, 16:03:29 UTC |
| 2c7b624 | 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:02 UTC |
| 002aa84 | Pierre-Yves Strub | 14 December 2015, 14:21:43 UTC | Do not clear local hyps when generalized as-is. | 14 December 2015, 14:21:43 UTC |
| 495d125 | Pierre-Yves Strub | 14 December 2015, 12:02:17 UTC | Removing internal implem. of removed `move=> x!` | 14 December 2015, 12:02:17 UTC |
| b3c7360 | 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:58:56 UTC |
| 7f0c994 | Pierre-Yves Strub | 14 December 2015, 11:58:14 UTC | Removing (from parser) intro-patterm `x!` (unused) | 14 December 2015, 11:58:14 UTC |
| 0cc8001 | Pierre-Yves Strub | 14 December 2015, 11:38:27 UTC | Lexems `<-`, `->`, `<<-`, `->>` can now be glued together. | 14 December 2015, 11:38:36 UTC |
| d704fd7 | 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, 10:21:39 UTC |
| 87ea673 | Pierre-Yves Strub | 14 December 2015, 10:13:15 UTC | Lists: subseq + more on sorts. Some admits in subseq. | 14 December 2015, 10:13:23 UTC |
| 059c81d | Benjamin Gregoire | 14 December 2015, 04:36:01 UTC | generalize lemma | 14 December 2015, 04:36:10 UTC |
