| 74d19dd | Pierre-Yves Strub | 29 January 2016, 09:20:18 UTC | make von Neumann an abstract theory | 29 January 2016, 13:27:23 UTC |
| 09e92e3 | Pierre-Yves Strub | 29 January 2016, 07:40:57 UTC | Simplifying von Neumann example. | 29 January 2016, 13:27:23 UTC |
| acd25c7 | François Dupressoir | 28 January 2016, 10:40:01 UTC | Filling in an admit. This is to get familiar with summability. The proof needs looked at. | 28 January 2016, 10:40:01 UTC |
| f21ba4c | Pierre-Yves Strub | 27 January 2016, 16:17:20 UTC | internal API change for checking formula in *hl goals | 27 January 2016, 16:17:27 UTC |
| e379fcf | François Dupressoir | 27 January 2016, 09:41:04 UTC | Modernizing dinter and updating stdlib. | 27 January 2016, 09:41:04 UTC |
| 729da1a | Pierre-Yves Strub | 27 January 2016, 00:16:58 UTC | Cleaning a bit br93. (nothing deep) | 27 January 2016, 00:16:58 UTC |
| 60dffa8 | Pierre-Yves Strub | 27 January 2016, 00:10:32 UTC | BR93 is back- but still ugly. | 27 January 2016, 00:10:39 UTC |
| 4cafb1e | François Dupressoir | 26 January 2016, 18:48:48 UTC | One more example re-established. | 26 January 2016, 18:48:48 UTC |
| f4d55f0 | François Dupressoir | 26 January 2016, 18:43:59 UTC | Nits in DProd. | 26 January 2016, 18:43:59 UTC |
| b639c79 | François Dupressoir | 26 January 2016, 16:42:20 UTC | Minor cleanup in DList. | 26 January 2016, 16:42:20 UTC |
| 69e4fff | François Dupressoir | 26 January 2016, 16:41:20 UTC | Dropping DEmpty and DUnit. Use dnull and MUnit.dunit from NewDistr instead. | 26 January 2016, 16:41:20 UTC |
| bb6e7f1 | François Dupressoir | 26 January 2016, 16:27:38 UTC | Fixing examples that currently work w.r.t. new product distribution. | 26 January 2016, 16:27:38 UTC |
| c5c4f43 | François Dupressoir | 26 January 2016, 16:27:18 UTC | Switching to NewDistr for product distributions. | 26 January 2016, 16:27:18 UTC |
| 046650e | François Dupressoir | 26 January 2016, 15:59:57 UTC | Sampling in DProd and sampling both components are equivalent. | 26 January 2016, 15:59:57 UTC |
| 12bcb32 | François Dupressoir | 26 January 2016, 11:51:23 UTC | Maintaining examples that currently go through. | 26 January 2016, 11:51:23 UTC |
| ab26ad8 | François Dupressoir | 26 January 2016, 11:50:52 UTC | Distribution-filtering is now predicate-based. Fixing stdlib for this and other commits. | 26 January 2016, 11:50:52 UTC |
| ec15d84 | Pierre-Yves Strub | 25 January 2016, 21:48:31 UTC | At the end of `crush`, don't use delta when simplify. | 25 January 2016, 21:48:50 UTC |
| 93cd53b | François Dupressoir | 25 January 2016, 21:06:21 UTC | Updating vonNeumann to use new Dexcepted. Issues introduced by an earlier commit on `crush` are also fixed here. | 25 January 2016, 21:06:34 UTC |
| 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 |
