| 863066b | Pierre-Yves Strub | 23 September 2015, 08:28:02 UTC | Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec` [fix #17249] | 23 September 2015, 08:28:02 UTC |
| 8128994 | Pierre-Yves Strub | 23 September 2015, 08:13:42 UTC | Refactor flags declaration. new flags can now be added by declaring them in the `EcScope.KnownFlags` module. | 23 September 2015, 08:19:50 UTC |
| b0260a0 | François Dupressoir | 15 September 2015, 09:23:58 UTC | Cleanup in MEE-CBC example. | 15 September 2015, 13:21:36 UTC |
| 15d9bc2 | Pierre-Yves Strub | 15 September 2015, 10:33:34 UTC | build-linux: nits. | 15 September 2015, 10:33:34 UTC |
| d7f94f2 | Pierre-Yves Strub | 15 September 2015, 09:01:07 UTC | build-linux: nits. | 15 September 2015, 09:01:07 UTC |
| aa8a78e | Pierre-Yves Strub | 14 September 2015, 10:40:49 UTC | Fix detection of unused memory annotations. | 14 September 2015, 10:41:04 UTC |
| f5f8654 | Pierre-Yves Strub | 14 September 2015, 10:40:10 UTC | Internal API: add missing basic fol. destructors. | 14 September 2015, 10:41:04 UTC |
| ff42d24 | François Dupressoir | 10 September 2015, 18:08:23 UTC | A compositional proof example with some generic instantiations: MEE-CBC. | 12 September 2015, 10:10:01 UTC |
| ed479d3 | Pierre-Yves Strub | 11 September 2015, 09:40:05 UTC | In `sp`, substitute in the pre when simplifying assoc-list. [fix #17243] | 11 September 2015, 09:40:05 UTC |
| 5822d18 | Pierre-Yves Strub | 09 September 2015, 12:15:36 UTC | Pretty-printing: print the `nosmt` annotation when relevant. [fix #17242] | 09 September 2015, 12:15:36 UTC |
| 70dbe23 | Pierre-Yves Strub | 08 September 2015, 18:34:41 UTC | In `clone import`, import theory before creating realization scopes. [fix #17241] | 08 September 2015, 18:34:41 UTC |
| 143a21e | Pierre-Yves Strub | 06 September 2015, 08:21:51 UTC | `dump`: add an extra point to the extracted tactic. | 06 September 2015, 08:22:04 UTC |
| 9e8857c | François Dupressoir | 02 September 2015, 16:01:44 UTC | Make conseq options optional. [ref #17087] | 02 September 2015, 16:01:44 UTC |
| 20a0cf5 | Pierre-Yves Strub | 02 September 2015, 15:06:27 UTC | `conseq` now defaults to `conseq *` `conseq` takes a `frame` option, that default to `true`. Old behaviour of `conseq` can be obtained using `conseq [-frame]`. [close #17087] | 02 September 2015, 15:06:45 UTC |
| 5a06269 | Pierre-Yves Strub | 02 September 2015, 15:01:55 UTC | BLURP | 02 September 2015, 15:01:55 UTC |
| 2636b3d | Pierre-Yves Strub | 02 September 2015, 14:02:32 UTC | Print anonymous variable in a way s.t. they can be distinguished. | 02 September 2015, 14:02:32 UTC |
| 230333d | Pierre-Yves Strub | 02 September 2015, 13:45:10 UTC | Auto-revert intro-pattern: fix ordering of reverts. | 02 September 2015, 13:45:10 UTC |
| c71618b | Pierre-Yves Strub | 02 September 2015, 13:12:16 UTC | New implicit view: (f1 <=> f2) => f2 => f1. | 02 September 2015, 13:12:16 UTC |
| 8475041 | Pierre-Yves Strub | 02 September 2015, 10:47:56 UTC | Restrict choice operators to lemmas that doesn't use local/abs modules. [fix #17168] | 02 September 2015, 10:47:56 UTC |
| 2fb8cf0 | Pierre-Yves Strub | 02 September 2015, 10:41:20 UTC | Scope restrictions now apply to operators/predicates/types. Moreover, all types appearing in internal form/expr nodes are checked for restrictions violations. [fix #17148] | 02 September 2015, 10:41:20 UTC |
| 03bd07b | Pierre-Yves Strub | 02 September 2015, 09:28:51 UTC | Fix intro-pattern `+` raising low-level exceptions when cannot revert/clear. In case a variable cannot be reverted (for dependency issues), it is generalized and the former (anonymous variable) is kept as such. This behaviour may change in the future, do not rely on it. [fix #17238] | 02 September 2015, 09:28:51 UTC |
| 14e1307 | Pierre-Yves Strub | 02 September 2015, 09:16:23 UTC | Internal API: `t_clear(s)` now has a mode for not failing on clear error. In that case, the clear is simply ignored instead of raising a low-level exception. | 02 September 2015, 09:26:10 UTC |
| 90f976e | Pierre-Yves Strub | 29 August 2015, 10:19:48 UTC | `delta` intro-pattern Syntax is `-?{occ}?/fterm` and is equivalent to its `rewrite` counter-part. | 29 August 2015, 10:19:48 UTC |
| 4f52b26 | Pierre-Yves Strub | 29 August 2015, 07:44:55 UTC | Auto-revert intro-pattern The intro-pattern `+` introduce the top-assumption under an anonymous name and revert it back at the end of the intro. process. Names of forall-bound variables are kept when reverting. This allows the application of view to assumptions that are below the top-assumption, as in `move=> + + /view`. | 29 August 2015, 07:45:59 UTC |
| d04aaff | Pierre-Yves Strub | 29 August 2015, 05:16:09 UTC | PLUS is the symbol for addition. | 29 August 2015, 05:16:09 UTC |
| 35537bb | Pierre-Yves Strub | 29 August 2015, 03:19:07 UTC | Use right environment for typing rewrite rule in `rewrite ... in ...` The environment should be the prefix env. above the `rewrite` target. [fix #17237] | 29 August 2015, 03:19:07 UTC |
| 4392eb2 | Pierre-Yves Strub | 28 August 2015, 06:37:46 UTC | Why3 version bump | 28 August 2015, 06:38:13 UTC |
| 614d43a | François Dupressoir | 25 August 2015, 08:15:05 UTC | PG keywords | 25 August 2015, 08:15:05 UTC |
| 212f33b | Pierre-Yves Strub | 21 August 2015, 15:23:06 UTC | cloning: regexp based renamings Work for types, operators, predicates, modules and module types. The syntax is: - `clone ... rename [class1, ...] "regexp" to "subst" ...` - `clone ... rename "regexp" to "subst" ...` where `class_i` is in `type`, `op`, `pred`, `module` and `module type`. The `rename` clause applies the regexp to all the object names of the cloned theories, whose class matches one of the given classes (or regardless of the object class if no classes are given). If the regexp matches, the new object name is given by the substitution pattern. Once a rename clause matches, no more renaming is performed for the object (i.e. the mechanism as a first match semantics). See the PCRE documentation for help about the regexp and substitution syntax. Note that the $0 substitution pattern is forbidden. [close #17182]. Reopen the ticket is more renaming mechanisms are needed. | 21 August 2015, 15:23:06 UTC |
| f14beaa | Pierre-Yves Strub | 20 August 2015, 18:13:45 UTC | pp: goalline width onw depends on terminal width. | 20 August 2015, 18:13:45 UTC |
| 24c5f8d | Pierre-Yves Strub | 20 August 2015, 17:58:50 UTC | nits in goal dump. | 20 August 2015, 17:59:04 UTC |
| a0e584c | François Dupressoir | 20 August 2015, 11:36:56 UTC | Pushing the dangerous smt call slightly further in NewFMap. No time to go add the general lemmas regarding assoc, index and to NewList. | 20 August 2015, 11:36:56 UTC |
| e0343fd | François Dupressoir | 20 August 2015, 11:24:52 UTC | Fixing test cases for syntactic changes. | 20 August 2015, 11:24:52 UTC |
| 7a6cb52 | François Dupressoir | 20 August 2015, 11:21:37 UTC | Fix NewPRP/PRF | 20 August 2015, 11:21:37 UTC |
| 1cd234a | François Dupressoir | 20 August 2015, 11:20:43 UTC | Fix old FMap | 20 August 2015, 11:20:43 UTC |
| e7ab0b0 | François Dupressoir | 20 August 2015, 11:18:37 UTC | Fixing NewList. | 20 August 2015, 11:18:37 UTC |
| 9b434e1 | François Dupressoir | 20 August 2015, 11:16:08 UTC | Fixing Poly. | 20 August 2015, 11:16:22 UTC |
| 2a01d4d | Pierre-Yves Strub | 20 August 2015, 10:14:50 UTC | Makefile (nits) | 20 August 2015, 10:14:50 UTC |
| 31dc05b | Pierre-Yves Strub | 20 August 2015, 07:20:48 UTC | `width` argument for the `dump` command. | 20 August 2015, 07:20:48 UTC |
| bb223e0 | Pierre-Yves Strub | 20 August 2015, 07:12:14 UTC | Finalize implementation of `dump` | 20 August 2015, 07:12:14 UTC |
| 28694ef | Pierre-Yves Strub | 19 August 2015, 19:27:18 UTC | New vernacular command: `dump` `dump "filename" (tactic)` aims at dumping to - filename.ec: the tactic executed - filename.0.ec: the initial goal - filename.$i.ec: the i-th goal after application of the tactic In interactive mode (i.e. with stdin at its input), the tactic raw-text cannot be read back and `filename.ec` is empty. WARN: the generation of `filename.$i.ec` is not yet working. | 19 August 2015, 19:27:18 UTC |
| de23cab | Pierre-Yves Strub | 18 August 2015, 15:03:09 UTC | Emit warnings when a memory marker is unused. The warning is currently emitted as soon as the problem is detected. We may want to defer them. [close #16055] | 18 August 2015, 15:03:09 UTC |
| 6ca1f59 | Pierre-Yves Strub | 18 August 2015, 13:28:50 UTC | New parsing rule for abstract pred. declaration Syntax is `pred : stype & ... & stype` | 18 August 2015, 13:28:50 UTC |
| 6ef4777 | Pierre-Yves Strub | 18 August 2015, 13:10:37 UTC | Parser nits. [fix #17235] | 18 August 2015, 13:10:37 UTC |
| f60ad80 | Pierre-Yves Strub | 18 August 2015, 13:09:55 UTC | `proc` return type is now optional. [close #17234] | 18 August 2015, 13:09:55 UTC |
| 4f6f2f1 | Pierre-Yves Strub | 18 August 2015, 11:25:40 UTC | Update license info. | 18 August 2015, 11:25:40 UTC |
| b207729 | Pierre-Yves Strub | 18 August 2015, 11:11:43 UTC | Generate a warning when reading a (potentially) uninitialized var. [close #16964] | 18 August 2015, 11:12:28 UTC |
| 4eb50dd | Pierre-Yves Strub | 17 August 2015, 09:02:04 UTC | Refactoring: code style of EcModules. | 17 August 2015, 09:39:58 UTC |
| 4273ce9 | Pierre-Yves Strub | 14 August 2015, 09:15:45 UTC | fr2en | 14 August 2015, 09:15:45 UTC |
| 978b840 | Pierre-Yves Strub | 12 August 2015, 21:53:38 UTC | Fix bug in operators selection. Selection was improperly detecting is an operator name was in the currently defined theory or not. | 12 August 2015, 21:53:38 UTC |
| cb39586 | Pierre-Yves Strub | 10 August 2015, 15:25:54 UTC | Fix bug in operators selection. All operators have to be returned when no operators match in the current theory. [fix #17230] | 10 August 2015, 15:25:54 UTC |
| eefe9ef | Pierre-Yves Strub | 10 August 2015, 13:06:16 UTC | Improve datatype emptyness check. When using external types in datatypes constructors' types, we now use their definition to check for emptiness instead of considering them abstract. [fix #17231] | 10 August 2015, 13:06:16 UTC |
| 4b68fab | Pierre-Yves Strub | 07 August 2015, 12:58:30 UTC | Don't fully-qualified local variable names. [ref #17233] | 07 August 2015, 12:58:30 UTC |
| 8ef77a8 | Pierre-Yves Strub | 07 August 2015, 12:11:54 UTC | More on pretty-printing of modules [ref #17233] | 07 August 2015, 12:11:54 UTC |
| ec8e5ed | Pierre-Yves Strub | 07 August 2015, 12:11:38 UTC | Fix ordering of module items in typing. | 07 August 2015, 12:11:38 UTC |
| e31a2f1 | Pierre-Yves Strub | 07 August 2015, 10:59:53 UTC | Fully reworked the pretty-printing of modules/proc. [ref #17233] | 07 August 2015, 10:59:53 UTC |
| 733e2f5 | Pierre-Yves Strub | 07 August 2015, 10:00:04 UTC | Fix priority (in pp) of _?_:_ [ref #17233] | 07 August 2015, 10:00:04 UTC |
| 955e909 | Pierre-Yves Strub | 30 July 2015, 08:20:28 UTC | NewList: last_ -> last. | 30 July 2015, 08:20:28 UTC |
| 08d27bb | Pierre-Yves Strub | 30 July 2015, 08:19:07 UTC | Some keywords can now be idents. The current list is: first, last, left, right, expect, strict. | 30 July 2015, 08:19:07 UTC |
| c557b9f | Pierre-Yves Strub | 30 July 2015, 07:54:20 UTC | README.md: add instructions for PCRE. | 30 July 2015, 07:54:20 UTC |
| 2df2da9 | Pierre-Yves Strub | 29 July 2015, 22:10:07 UTC | Fix various pretty printing bugs. [fix #17229] | 29 July 2015, 22:10:07 UTC |
| 393f6e3 | Pierre-Yves Strub | 29 July 2015, 19:01:55 UTC | Misc. fix in pretty printer [fix #17228] | 29 July 2015, 19:01:55 UTC |
| 04ccfc4 | Pierre-Yves Strub | 29 July 2015, 07:16:24 UTC | Don't prevent users to return a unit value in proc. [close #17227] | 29 July 2015, 07:16:24 UTC |
| 5945f0b | Pierre-Yves Strub | 28 July 2015, 13:58:12 UTC | Move to PCRE. [ref #17182]: renaming is going to take PCRE expressions, so better moving from Str to PCRE once and for all. Depends on ocaml-pcre (toolchain: 20150728) | 28 July 2015, 13:58:55 UTC |
| b0395bf | Benedikt Schmidt | 28 July 2015, 12:43:34 UTC | clean up Hybrid theories (results are still the same modulo renaming of modules) | 28 July 2015, 12:43:44 UTC |
| c2523f3 | Pierre-Yves Strub | 28 July 2015, 11:13:31 UTC | axiom can now be tagged for better proof specification in cloning. Axioms can now be tagged with a set of symbols. The syntax is: `axiom [tag1 tag2...]? nosmt? name : spec.` In theory cloning, catch-all proof specification can be also tagged. The syntax is: `clone ... proof T.* [tag1 tag2...]?` The proof specification is then only applied to axioms whose tags have a non-empty intersection with the proof specification tags. (If no tags are provided, the old behavior is obtained - i.e. the proof specification is applied unconditionally). It is now allowed to give multiple starred proof-specifications. If so, the first proof-specification matching is applied. [close #17165] | 28 July 2015, 11:13:31 UTC |
| 96e855d | Pierre-Yves Strub | 28 July 2015, 09:42:47 UTC | Remove unused `hypothesis` keyword. | 28 July 2015, 09:43:12 UTC |
| 61eb46a | François Dupressoir | 28 July 2015, 08:41:00 UTC | Extending base of results on last_ | 28 July 2015, 08:41:08 UTC |
| daca4c9 | Pierre-Yves Strub | 28 July 2015, 07:01:20 UTC | Remove unused parse rules. | 28 July 2015, 07:01:20 UTC |
| 445abc1 | Pierre-Yves Strub | 27 July 2015, 19:47:44 UTC | Misc. fix of pretty printer - Fix associativity of :: - Fix pretty-printer of operator names (in printing of op. decl) - Add a space between a unary operator and its argument if this last is not a terminal symbol - Warn when a unary/binary operator cannot be used in prefix/infix mode [fix #17226] | 27 July 2015, 20:46:58 UTC |
| c53f776 | Pierre-Yves Strub | 26 July 2015, 21:38:07 UTC | Define BigAlg as an exntesion of BigOp. | 26 July 2015, 21:38:07 UTC |
| c6cf91d | Pierre-Yves Strub | 26 July 2015, 13:59:58 UTC | Add support for pattern (op-fix) in infix form. [fix #16786] | 26 July 2015, 20:15:41 UTC |
| 0a937a8 | Pierre-Yves Strub | 26 July 2015, 09:14:52 UTC | Add a exn. printer for lexical errors + improve lex error msgs. [fix #17223, #17224] | 26 July 2015, 09:15:43 UTC |
| 54fa7c1 | Pierre-Yves Strub | 25 July 2015, 09:55:37 UTC | Use alpha-eq. when searching for a contradiction in context. [close #17179] | 25 July 2015, 09:55:37 UTC |
| 8853bf3 | Pierre-Yves Strub | 21 July 2015, 21:06:09 UTC | Add a pragma to restart EasyCrypt. The pragma is `restart`. W.r.t `reset`, `restart` forces the reload of the prelude. [fix #17213] | 21 July 2015, 21:06:09 UTC |
| 49ffdf3 | Pierre-Yves Strub | 21 July 2015, 16:27:54 UTC | Negative line selector in program tactics. Line `-1` is the last line, `-2` the penultimate one, and so on. [close #17059] | 21 July 2015, 16:27:54 UTC |
| abed2a9 | Pierre-Yves Strub | 17 July 2015, 14:33:08 UTC | Better user error message when giving an invalid inv. to `call`. [fix #17110] | 17 July 2015, 14:33:08 UTC |
| 787e2ad | Pierre-Yves Strub | 17 July 2015, 10:46:34 UTC | In expressions (in proc.), give priority to program vars. [fix #17189] | 17 July 2015, 10:46:34 UTC |
| 80265d2 | Pierre-Yves Strub | 17 July 2015, 10:25:39 UTC | Activate OCaml exception based CLI interruption. This is drafty as the SIGINT signal should be masked most of the time and only unmasked at very specific cancelation points. Mainly: before each tactical invocation and during SMT calls. [ref #17082] | 17 July 2015, 10:25:39 UTC |
| 6336362 | Pierre-Yves Strub | 17 July 2015, 09:28:44 UTC | Detection of circular deps. [fix #17212] | 17 July 2015, 09:28:44 UTC |
| f0c7ded | Pierre-Yves Strub | 17 July 2015, 07:39:10 UTC | Refactor-in printing functions. | 17 July 2015, 07:39:10 UTC |
| f37ef90 | Pierre-Yves Strub | 14 July 2015, 15:43:51 UTC | Fix pretty-printing of oracle informations. [ref #17215] | 14 July 2015, 15:44:05 UTC |
| 9f6601d | Pierre-Yves Strub | 13 July 2015, 10:28:18 UTC | Add a command to dump the full Why3 task This dumps the full environment, no hypothesis selection is done, and the `nosmt` flag is ignored. [close #17196] | 13 July 2015, 10:28:18 UTC |
| 25d7504 | Pierre-Yves Strub | 11 July 2015, 19:03:40 UTC | Pretty-printing of match-fix. [fix #17219] | 12 July 2015, 12:14:23 UTC |
| 9b8598c | Pierre-Yves Strub | 11 July 2015, 18:16:06 UTC | Set log-level to at least Warning when loading a theory. | 12 July 2015, 12:14:13 UTC |
| 52c261b | Pierre-Yves Strub | 11 July 2015, 18:08:43 UTC | Fix pretty-printer of abstract predicates, Don't print their type as for boolean operators, as the parser do not accept this syntax. [ref #17219] | 12 July 2015, 12:13:46 UTC |
| a56587b | Pierre-Yves Strub | 11 July 2015, 17:59:05 UTC | Add `realize name by tactics` syntax Similiar to `lemma name : spec by tactics`, but applied to realization of lemmas after a partial clone. [fix #17220] | 12 July 2015, 12:13:35 UTC |
| 8a89d9d | Pierre-Yves Strub | 11 July 2015, 17:31:06 UTC | Syntax change `lemma L : F by t` now takes a tactic sequence instead of a single tactic. [fix #17221] | 12 July 2015, 12:13:22 UTC |
| ca59aac | Pierre-Yves Strub | 11 July 2015, 17:27:16 UTC | New reduction rule for equality over unit. `x = y --> true` when `x, y : unit`. | 12 July 2015, 12:12:48 UTC |
| 1a35e05 | Pierre-Yves Strub | 10 July 2015, 20:30:10 UTC | StdRing: nosmt. | 10 July 2015, 20:30:18 UTC |
| e3f7ce1 | Pierre-Yves Strub | 10 July 2015, 20:12:56 UTC | Ring/Number: trivial lemmas. | 10 July 2015, 20:13:11 UTC |
| d89a5af | Pierre-Yves Strub | 10 July 2015, 20:12:45 UTC | FSet: pick + trivial lemmas. | 10 July 2015, 20:13:09 UTC |
| bdab7b1 | Pierre-Yves Strub | 10 July 2015, 20:12:32 UTC | Add some if-construct simplification lemmas. | 10 July 2015, 20:13:08 UTC |
| 536b08d | Pierre-Yves Strub | 10 July 2015, 15:37:23 UTC | finset: subset <-> card relation. | 10 July 2015, 15:37:36 UTC |
| 3282164 | Pierre-Yves Strub | 10 July 2015, 15:37:10 UTC | More facts on the zmodule op. | 10 July 2015, 15:37:35 UTC |
| ce05b75 | Pierre-Yves Strub | 09 July 2015, 10:20:38 UTC | Remove reserved keywords from uniop | 09 July 2015, 10:21:32 UTC |
| abf3561 | François Dupressoir | 09 July 2015, 09:44:00 UTC | Array: fix and prove make_append. | 09 July 2015, 09:44:00 UTC |
| c61b653 | Pierre-Yves Strub | 07 July 2015, 14:32:22 UTC | NewFSet: core lemmas about cardinal. | 07 July 2015, 14:32:22 UTC |
| 880c7a0 | Pierre-Yves Strub | 07 July 2015, 14:07:25 UTC | Cleaning NewFSet a bit. | 07 July 2015, 14:07:25 UTC |
| 127bc94 | Pierre-Yves Strub | 07 July 2015, 13:37:21 UTC | Import basic theory of membership and finite sets. | 07 July 2015, 13:37:21 UTC |
