| 7585325 | Pierre-Yves Strub | 22 March 2015, 15:07:25 UTC | Fix `catch` clause not catching the right exception [fix #17187]: anomaly when invalid memory is referenced | 22 March 2015, 15:07:25 UTC |
| 41f0016 | Pierre-Yves Strub | 10 March 2015, 14:28:05 UTC | New SMT tactic. This commit brings a new `smt` tactic that can be called via `smt:lazy`. This tactic relies on a lazy translation of operators/lemmas and is currently missing: - a proper selection of lemmas to sent - the translation of body of fixpoints - a set of flags to better control the translation (including the use of the already existing hints databases) The default `smt` version to be called can be controlled via the `Smt:lazy` option. By default, the legacy version is used. If changed to the new one, the old one can be locally called via the `smt:full` variant of `smt`. This commit also bring a `time` meta command that can be used to time any vernacular command by simply executing: `time thecommand.` | 20 March 2015, 15:44:19 UTC |
| 39d4a0b | Pierre-Yves Strub | 18 March 2015, 23:16:01 UTC | Add a report URL. [fix #17185] | 18 March 2015, 23:16:01 UTC |
| 2fbf6c7 | François Dupressoir | 16 March 2015, 13:43:38 UTC | Doc: adding 'have', some minor things in other tactics. | 16 March 2015, 13:43:38 UTC |
| 4797bab | François Dupressoir | 16 March 2015, 12:06:37 UTC | Folding array notations into NewList.Array. | 16 March 2015, 12:06:37 UTC |
| 48d7d3d | François Dupressoir | 16 March 2015, 11:26:27 UTC | Reorg NewFMap: now operator-complete (modulo unary versions of find and map). | 16 March 2015, 11:26:27 UTC |
| 4125d5b | François Dupressoir | 12 March 2015, 15:04:32 UTC | NewFMap: new pass over proofs, changes to eq_except. eq_except now takes a set of keys on which maps may disagree; this should allow lemmas relating join, filter and eq_except. | 12 March 2015, 15:04:32 UTC |
| b541d6a | François Dupressoir | 12 March 2015, 11:56:01 UTC | NewFMap: pass over proofs. | 12 March 2015, 11:56:01 UTC |
| 4be0508 | François Dupressoir | 12 March 2015, 10:30:30 UTC | NewFMap: filter and map definitions and core lemmas. | 12 March 2015, 10:30:30 UTC |
| a574f39 | François Dupressoir | 10 March 2015, 11:52:47 UTC | Hops. | 10 March 2015, 11:52:47 UTC |
| 261f326 | François Dupressoir | 09 March 2015, 16:32:34 UTC | More comp -> \o | 09 March 2015, 16:32:34 UTC |
| e3d8167 | François Dupressoir | 09 March 2015, 14:57:19 UTC | A push on arrays. Realization: arrays do not need to exist. At all. All we need is set and mapi operators on lists. Everything else is notation. | 09 March 2015, 14:57:19 UTC |
| d5af99d | François Dupressoir | 09 March 2015, 12:12:58 UTC | comp -> \o | 09 March 2015, 12:12:58 UTC |
| 5e94343 | Pierre-Yves Strub | 07 March 2015, 22:17:24 UTC | In `clone`, `proof *` does not catch axioms in abstract theories anymore. | 07 March 2015, 22:17:24 UTC |
| 9745703 | Pierre-Yves Strub | 06 March 2015, 16:06:03 UTC | Progressing on algebraic hierarchy. | 06 March 2015, 16:06:03 UTC |
| 8680abb | Pierre-Yves Strub | 06 March 2015, 14:32:49 UTC | When reducing a beta-redex, also reduce created beta-redexes. [fix #17091] | 06 March 2015, 14:32:59 UTC |
| ed135cc | Pierre-Yves Strub | 06 March 2015, 09:41:40 UTC | Change operators selection When there is an ambiguity, give precedence to operators that have been defined in the currently defined theory. | 06 March 2015, 14:32:59 UTC |
| 2e03fe2 | Pierre-Yves Strub | 06 March 2015, 08:31:03 UTC | Don't introduce implicit arguments when no explicit ones are given. | 06 March 2015, 14:32:59 UTC |
| c9a31a1 | François Dupressoir | 05 March 2015, 16:06:34 UTC | NewArray: redefining set (as a fixpoint). Better start. | 05 March 2015, 16:06:34 UTC |
| 644aa5b | François Dupressoir | 05 March 2015, 13:12:58 UTC | Fixing yet another copy-paste... *shakes fist at PY* | 05 March 2015, 13:12:58 UTC |
| 97ca7d6 | François Dupressoir | 05 March 2015, 10:09:17 UTC | NewFMap: eq_except starts. | 05 March 2015, 10:09:17 UTC |
| 755567f | Pierre-Yves Strub | 04 March 2015, 15:56:47 UTC | Fixing smt failures in Ring.ec. | 04 March 2015, 15:56:47 UTC |
| 8f2e25e | Pierre-Yves Strub | 04 March 2015, 14:13:11 UTC | Flatten algebraic hierarchy using `clone include`. | 04 March 2015, 14:13:11 UTC |
| b87eecb | Pierre-Yves Strub | 04 March 2015, 14:04:43 UTC | Fix (weak) issues in stdlib (but in encryption/) | 04 March 2015, 14:04:43 UTC |
| 66d26c3 | Pierre-Yves Strub | 04 March 2015, 14:00:01 UTC | Makefile: new target (weak-check) for fast checking standard library. | 04 March 2015, 14:00:01 UTC |
| 3082bcf | Pierre-Yves Strub | 04 March 2015, 13:50:24 UTC | `clone include` `clone include` allows to include the body of a cloned theory into the current defined one. The main purpose is to avoid long names while chaining clonings. E.g.: {{{ abstract theory ZModule. type t. op zero : t. op add: t -> t -> t. op opp: t -> t. axiom addr0 (x : t): add x zero = x. end ZModule. abstract theory Ring. clone include ZModule. op one : t. op mul : t -> t -> t. ... end Ring. clone Ring as IntRing with type t <- int, ... }}} In that version, `addr0` (of IntRing) fullname is `IntRing.addr0`, not `IntRing.ZModule.addr0`. | 04 March 2015, 13:51:41 UTC |
| 7cc0638 | François Dupressoir | 04 March 2015, 11:50:01 UTC | Hybrid argument: all adapted except for bigop-related argument in Hybrid.ec | 04 March 2015, 11:50:01 UTC |
| 2fff1fc | François Dupressoir | 04 March 2015, 11:32:01 UTC | ExtEq: rename [eq_refl], [eq_symm] and [eq_tran] to avoid clashes. | 04 March 2015, 11:32:01 UTC |
| 5ffedd8 | Pierre-Yves Strub | 03 March 2015, 16:03:15 UTC | printf removed. | 03 March 2015, 16:03:22 UTC |
| 759043e | François Dupressoir | 03 March 2015, 13:38:52 UTC | More progress on maps: removing admits. One unstable smt call. | 03 March 2015, 13:39:03 UTC |
| 03c51dd | François Dupressoir | 03 March 2015, 11:19:46 UTC | Fix in NewList. Some progress in NewFMap. | 03 March 2015, 13:39:02 UTC |
| 310697b | Pierre-Yves Strub | 03 March 2015, 11:50:34 UTC | Refactoring of subst + refresh introduced locals when elim. a existential. [fix #17180] | 03 March 2015, 11:54:05 UTC |
| da5f2b8 | François Dupressoir | 02 March 2015, 17:37:32 UTC | Starting to expand: just lemmas (some proofs missing). | 02 March 2015, 17:37:32 UTC |
| 4f48ab4 | François Dupressoir | 02 March 2015, 14:54:26 UTC | Finishing with the consequences of reduction changes. All failures left are either wanted (NewList), due to the switch to IntExtra (Ring), or of unknown status (encryption/*). | 02 March 2015, 14:54:26 UTC |
| 95d755e | François Dupressoir | 02 March 2015, 12:02:03 UTC | Starting a pass after changes in reduction. | 02 March 2015, 12:02:03 UTC |
| b150a61 | Pierre-Yves Strub | 27 February 2015, 22:23:10 UTC | Revert "temporary hack to have from_int from `Real` and `NewReal`." This reverts commit 001b85cd74c722c3e2870f079e2cc77ad3ff2227. | 27 February 2015, 22:23:10 UTC |
| f392969 | Pierre-Yves Strub | 27 February 2015, 20:59:44 UTC | Numerical series convergence (def) | 27 February 2015, 20:59:44 UTC |
| ff3872e | Pierre-Yves Strub | 27 February 2015, 20:55:02 UTC | Basic integral domain number theory for reals. | 27 February 2015, 20:55:02 UTC |
| 001b85c | Pierre-Yves Strub | 27 February 2015, 20:54:41 UTC | temporary hack to have from_int from `Real` and `NewReal`. | 27 February 2015, 20:54:41 UTC |
| 5d8f2d4 | Pierre-Yves Strub | 27 February 2015, 20:42:50 UTC | In `Ring`, tags all axioms with `nosmt` | 27 February 2015, 20:42:50 UTC |
| c8c17db | Pierre-Yves Strub | 27 February 2015, 20:42:26 UTC | `import / export` now takes a list of theory names. | 27 February 2015, 20:42:26 UTC |
| d6ff406 | Pierre-Yves Strub | 27 February 2015, 12:52:29 UTC | NewList: head/ohead operators + theory. | 27 February 2015, 12:52:39 UTC |
| 3664f9b | François Dupressoir | 26 February 2015, 10:14:10 UTC | NewFMap: rm and some more lemmas. | 26 February 2015, 10:14:10 UTC |
| d820bdc | François Dupressoir | 26 February 2015, 09:53:20 UTC | Generalize assoc_filter. | 26 February 2015, 09:53:20 UTC |
| 6f03862 | François Dupressoir | 25 February 2015, 17:31:54 UTC | NewArray: a first attempt that directly uses lists. Not sure where this is going to fail. | 25 February 2015, 17:31:54 UTC |
| 65cfde9 | Pierre-Yves Strub | 24 February 2015, 16:43:06 UTC | FMap: remove staled comments. | 24 February 2015, 16:43:06 UTC |
| 0853ab0 | Pierre-Yves Strub | 24 February 2015, 16:42:26 UTC | Inductive: in scheme generation, fix bug related to constructors attached types. | 24 February 2015, 16:42:30 UTC |
| 7866976 | Pierre-Yves Strub | 24 February 2015, 16:42:03 UTC | CoreFol: misc Mainly, when calling `f_app` with no arguments, do use the given result type insteadm of ignoring it. | 24 February 2015, 16:42:30 UTC |
| 2647e48 | François Dupressoir | 24 February 2015, 16:25:45 UTC | FMap: core lemmas | 24 February 2015, 16:25:45 UTC |
| ad88212 | Pierre-Yves Strub | 24 February 2015, 14:27:55 UTC | FMap: join / induction principle + nits. | 24 February 2015, 14:27:55 UTC |
| a9e1de4 | Pierre-Yves Strub | 24 February 2015, 11:38:54 UTC | NewFMap: fix all admits (w.r.t reduce) + extension to NewList (rev) | 24 February 2015, 11:38:54 UTC |
| 0962c9e | Pierre-Yves Strub | 24 February 2015, 00:47:10 UTC | NewFMap: piggy back to raw association lists. | 24 February 2015, 00:47:10 UTC |
| f841eae | Pierre-Yves Strub | 23 February 2015, 20:01:09 UTC | Clean NewFMap, pusing generic facts (about assoc) to NewList. | 23 February 2015, 20:01:09 UTC |
| 4e941db | Pierre-Yves Strub | 23 February 2015, 20:00:54 UTC | Logic: misc. (a big revamp is still needed) | 23 February 2015, 20:00:54 UTC |
| 4219b47 | Pierre-Yves Strub | 23 February 2015, 20:00:37 UTC | Int: basic facts that arises when doing nat-o-int induction. | 23 February 2015, 20:00:37 UTC |
| b7c2bca | Pierre-Yves Strub | 23 February 2015, 20:00:10 UTC | Extend reduction If `C` is a constructor, `C x1 ... xn = C y1 ... yn` reduces to `(x1 = y1 /\ ... /\ xn = yn)`. This reduction was already active for nullary constructors and tuples. | 23 February 2015, 20:00:10 UTC |
| 05ee246 | Pierre-Yves Strub | 23 February 2015, 13:30:04 UTC | Progress on lists + fmaps (partial) cleanup. | 23 February 2015, 13:30:04 UTC |
| 7ec25c2 | Pierre-Yves Strub | 23 February 2015, 13:29:49 UTC | New reduction: `!a <=> !b` reduces to `a <=> b`. | 23 February 2015, 13:29:49 UTC |
| 8275603 | Pierre-Yves Strub | 23 February 2015, 10:35:40 UTC | Fix stdlib + refactor a bit NewFMap. | 23 February 2015, 10:35:40 UTC |
| d3e2b6b | Pierre-Yves Strub | 23 February 2015, 09:38:25 UTC | Override List.sum / List.sumf. BatList.{sum,sumf} are raising an exception on empty lists, instead of returning 0. This behaviour is now overriden. | 23 February 2015, 09:38:25 UTC |
| 1630263 | Pierre-Yves Strub | 21 February 2015, 14:33:58 UTC | Makefile: fix purge target. | 21 February 2015, 14:33:58 UTC |
| 8cfb892 | Pierre-Yves Strub | 21 February 2015, 14:31:33 UTC | Makefile: install PG files. | 21 February 2015, 14:31:49 UTC |
| 593c49f | François Dupressoir | 20 February 2015, 16:29:54 UTC | Major progres on FMap: realizing that complexity is evil. | 20 February 2015, 23:28:11 UTC |
| 9089c0e | Pierre-Yves Strub | 20 February 2015, 23:19:55 UTC | Some facts about zmod-morphism / ring-morphism. These theories are hardly usable with type classes. Type-classes is now high-priority. | 20 February 2015, 23:19:55 UTC |
| e0b6d30 | Pierre-Yves Strub | 20 February 2015, 23:18:58 UTC | axiomatized by now generate an extentional equality scheme. | 20 February 2015, 23:18:58 UTC |
| ecc941f | Pierre-Yves Strub | 20 February 2015, 16:17:45 UTC | Use natind in NewList when possible. | 20 February 2015, 16:17:45 UTC |
| 2accade | Pierre-Yves Strub | 20 February 2015, 15:51:19 UTC | New libraries progress (lists / bigops). | 20 February 2015, 15:51:19 UTC |
| a0a3192 | Pierre-Yves Strub | 20 February 2015, 14:30:23 UTC | Update internal copyright. | 20 February 2015, 14:30:23 UTC |
| f3b47f9 | Pierre-Yves Strub | 20 February 2015, 14:29:45 UTC | Improving new theories (lists / bigops) | 20 February 2015, 14:29:45 UTC |
| 42dd869 | Pierre-Yves Strub | 20 February 2015, 13:10:19 UTC | Register `move` as a "non-case" tactic. Fix bug introduced by having `move` not backing anymore to `generalize` | 20 February 2015, 13:10:41 UTC |
| dfe82eb | Pierre-Yves Strub | 20 February 2015, 12:05:11 UTC | Fix admits in bigops. | 20 February 2015, 12:05:11 UTC |
| aa4ad9d | Pierre-Yves Strub | 20 February 2015, 11:33:53 UTC | Progress on new stdlib (lists / bigops) | 20 February 2015, 11:33:53 UTC |
| 4cedcb1 | Pierre-Yves Strub | 20 February 2015, 11:33:39 UTC | Basic extra lemmas about integers (comm-assoc, inversion) | 20 February 2015, 11:33:39 UTC |
| 83976d2 | Pierre-Yves Strub | 20 February 2015, 11:33:19 UTC | Add `have` as an alias to `cut`. | 20 February 2015, 11:33:19 UTC |
| 1d4260c | Pierre-Yves Strub | 20 February 2015, 08:59:52 UTC | Syntax change for tactics doing an implicit generalization The generalization patterns can now be prefixed by a colon (:) E.g., `case ptn` can be rewritten as `case:ptn`. | 20 February 2015, 08:59:52 UTC |
| 4111987 | Pierre-Yves Strub | 20 February 2015, 08:56:50 UTC | `move` can now takes postfixed views. Syntax if `move/view1/view2...`, and is identical to `move=> /view1 /view2 ...` Views are applied after any generalization. | 20 February 2015, 08:56:50 UTC |
| 6413482 | Pierre-Yves Strub | 19 February 2015, 21:16:19 UTC | NewList: element removal by index. | 19 February 2015, 21:16:19 UTC |
| ab12470 | Benjamin Gregoire | 19 February 2015, 19:02:14 UTC | word on iota | 19 February 2015, 19:02:37 UTC |
| a274763 | François Dupressoir | 19 February 2015, 17:35:24 UTC | Using reduce to fit with the expected representation of maps as association lists. | 19 February 2015, 17:35:31 UTC |
| 2220a40 | Pierre-Yves Strub | 19 February 2015, 17:04:47 UTC | Fix trash in NewList.ec | 19 February 2015, 17:04:47 UTC |
| d8ddcc6 | Pierre-Yves Strub | 19 February 2015, 17:04:39 UTC | View mechanism supports deconstructing <=>. | 19 February 2015, 17:04:39 UTC |
| 0b9a554 | Pierre-Yves Strub | 19 February 2015, 16:01:47 UTC | Bigop: refactoring, using new view mechanism. | 19 February 2015, 16:01:47 UTC |
| 7c619ff | Pierre-Yves Strub | 19 February 2015, 16:01:32 UTC | Fix bugs in intro view application + enchancement When applying a quantifed view, re-generalize uninstanciated parameters in the top assumption. | 19 February 2015, 16:01:32 UTC |
| f7601bd | Pierre-Yves Strub | 19 February 2015, 14:00:02 UTC | runtest: backport to python2 | 19 February 2015, 14:00:07 UTC |
| 533151b | Benjamin Gregoire | 19 February 2015, 12:15:57 UTC | add nosmt. | 19 February 2015, 13:36:51 UTC |
| 6a3bbfd | Pierre-Yves Strub | 19 February 2015, 13:21:08 UTC | Fix NewList compilation. | 19 February 2015, 13:21:14 UTC |
| d427269 | François Dupressoir | 18 February 2015, 19:57:57 UTC | Generalizing some of the lemmas to avoid duplicating too much effort. | 18 February 2015, 19:58:10 UTC |
| dcfa94b | Pierre-Yves Strub | 18 February 2015, 19:52:08 UTC | NewList / NewBigop | 18 February 2015, 19:52:08 UTC |
| f751db0 | Pierre-Yves Strub | 18 February 2015, 16:48:09 UTC | Fix stdlib | 18 February 2015, 16:48:09 UTC |
| 935e36c | Pierre-Yves Strub | 18 February 2015, 16:46:11 UTC | List: perm_eq_map | 18 February 2015, 16:46:11 UTC |
| fd32076 | Pierre-Yves Strub | 18 February 2015, 14:38:11 UTC | More bigop results. | 18 February 2015, 14:38:11 UTC |
| cd9d326 | Pierre-Yves Strub | 18 February 2015, 14:06:16 UTC | Support for implicits in `rewrite` | 18 February 2015, 14:06:16 UTC |
| d4269d6 | Pierre-Yves Strub | 18 February 2015, 12:01:54 UTC | Though on reducing association list in NewFMap. | 18 February 2015, 12:01:54 UTC |
| 4dea02e | Pierre-Yves Strub | 18 February 2015, 12:01:41 UTC | Seq: left folding. | 18 February 2015, 12:01:41 UTC |
| 09b0e75 | Pierre-Yves Strub | 18 February 2015, 11:50:00 UTC | Accept the syntax `fun x => e` for lambda abs. | 18 February 2015, 12:01:33 UTC |
| 2e767f9 | Pierre-Yves Strub | 18 February 2015, 11:28:12 UTC | Proper definition of big ops (no theory) | 18 February 2015, 11:28:21 UTC |
| 6745b0c | François Dupressoir | 18 February 2015, 10:38:37 UTC | dom and rng abstractions ready to go (modulo unicity of keys). | 18 February 2015, 10:38:46 UTC |
| 944ad05 | Pierre-Yves Strub | 18 February 2015, 10:12:11 UTC | Factor out and clean up comoid theory. | 18 February 2015, 10:12:17 UTC |
| 06c11be | Pierre-Yves Strub | 18 February 2015, 08:58:51 UTC | Factor out operator iteration from Ring to new theory IntExtra. | 18 February 2015, 10:12:17 UTC |
| baec8aa | Pierre-Yves Strub | 18 February 2015, 10:11:43 UTC | Induction/case analysis for natural numbers. - first version works in the case where the intended behaviour on negative numbers is identical to the one of 0. - second version is similar to the first one, but distinguishes the cases <0 and =0. | 18 February 2015, 10:12:17 UTC |
