sort by:
Revision Author Date Message Commit Date
863066b Ring axioms of the `ring`/`field` tactics agree with the ones of `` [fix #17249] 23 September 2015, 08:28 UTC
8128994 Refactor flags declaration. new flags can now be added by declaring them in the `EcScope.KnownFlags` module. 23 September 2015, 08:19 UTC
b0260a0 Cleanup in MEE-CBC example. 15 September 2015, 13:21 UTC
15d9bc2 build-linux: nits. 15 September 2015, 10:33 UTC
d7f94f2 build-linux: nits. 15 September 2015, 09:01 UTC
aa8a78e Fix detection of unused memory annotations. 14 September 2015, 10:41 UTC
f5f8654 Internal API: add missing basic fol. destructors. 14 September 2015, 10:41 UTC
ff42d24 A compositional proof example with some generic instantiations: MEE-CBC. 12 September 2015, 10:10 UTC
ed479d3 In `sp`, substitute in the pre when simplifying assoc-list. [fix #17243] 11 September 2015, 09:40 UTC
5822d18 Pretty-printing: print the `nosmt` annotation when relevant. [fix #17242] 09 September 2015, 12:15 UTC
70dbe23 In `clone import`, import theory before creating realization scopes. [fix #17241] 08 September 2015, 18:34 UTC
143a21e `dump`: add an extra point to the extracted tactic. 06 September 2015, 08:22 UTC
9e8857c Make conseq options optional. [ref #17087] 02 September 2015, 16:01 UTC
20a0cf5 `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 UTC
5a06269 BLURP 02 September 2015, 15:01 UTC
2636b3d Print anonymous variable in a way s.t. they can be distinguished. 02 September 2015, 14:02 UTC
230333d Auto-revert intro-pattern: fix ordering of reverts. 02 September 2015, 13:45 UTC
c71618b New implicit view: (f1 <=> f2) => f2 => f1. 02 September 2015, 13:12 UTC
8475041 Restrict choice operators to lemmas that doesn't use local/abs modules. [fix #17168] 02 September 2015, 10:47 UTC
2fb8cf0 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 UTC
03bd07b 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 UTC
14e1307 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 UTC
90f976e `delta` intro-pattern Syntax is `-?{occ}?/fterm` and is equivalent to its `rewrite` counter-part. 29 August 2015, 10:19 UTC
4f52b26 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 UTC
d04aaff PLUS is the symbol for addition. 29 August 2015, 05:16 UTC
35537bb 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 UTC
4392eb2 Why3 version bump 28 August 2015, 06:38 UTC
614d43a PG keywords 25 August 2015, 08:15 UTC
212f33b 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 UTC
f14beaa pp: goalline width onw depends on terminal width. 20 August 2015, 18:13 UTC
24c5f8d nits in goal dump. 20 August 2015, 17:59 UTC
a0e584c 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 UTC
e0343fd Fixing test cases for syntactic changes. 20 August 2015, 11:24 UTC
7a6cb52 Fix NewPRP/PRF 20 August 2015, 11:21 UTC
1cd234a Fix old FMap 20 August 2015, 11:20 UTC
e7ab0b0 Fixing NewList. 20 August 2015, 11:18 UTC
9b434e1 Fixing Poly. 20 August 2015, 11:16 UTC
2a01d4d Makefile (nits) 20 August 2015, 10:14 UTC
31dc05b `width` argument for the `dump` command. 20 August 2015, 07:20 UTC
bb223e0 Finalize implementation of `dump` 20 August 2015, 07:12 UTC
28694ef New vernacular command: `dump` `dump "filename" (tactic)` aims at dumping to - the tactic executed - the initial goal - filename.$ 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 `` is empty. WARN: the generation of `filename.$` is not yet working. 19 August 2015, 19:27 UTC
de23cab 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 UTC
6ca1f59 New parsing rule for abstract pred. declaration Syntax is `pred : stype & ... & stype` 18 August 2015, 13:28 UTC
6ef4777 Parser nits. [fix #17235] 18 August 2015, 13:10 UTC
f60ad80 `proc` return type is now optional. [close #17234] 18 August 2015, 13:09 UTC
4f6f2f1 Update license info. 18 August 2015, 11:25 UTC
b207729 Generate a warning when reading a (potentially) uninitialized var. [close #16964] 18 August 2015, 11:12 UTC
4eb50dd Refactoring: code style of EcModules. 17 August 2015, 09:39 UTC
4273ce9 fr2en 14 August 2015, 09:15 UTC
978b840 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 UTC
cb39586 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 UTC
eefe9ef 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 UTC
4b68fab Don't fully-qualified local variable names. [ref #17233] 07 August 2015, 12:58 UTC
8ef77a8 More on pretty-printing of modules [ref #17233] 07 August 2015, 12:11 UTC
ec8e5ed Fix ordering of module items in typing. 07 August 2015, 12:11 UTC
e31a2f1 Fully reworked the pretty-printing of modules/proc. [ref #17233] 07 August 2015, 10:59 UTC
733e2f5 Fix priority (in pp) of _?_:_ [ref #17233] 07 August 2015, 10:00 UTC
955e909 NewList: last_ -> last. 30 July 2015, 08:20 UTC
08d27bb Some keywords can now be idents. The current list is: first, last, left, right, expect, strict. 30 July 2015, 08:19 UTC
c557b9f add instructions for PCRE. 30 July 2015, 07:54 UTC
2df2da9 Fix various pretty printing bugs. [fix #17229] 29 July 2015, 22:10 UTC
393f6e3 Misc. fix in pretty printer [fix #17228] 29 July 2015, 19:01 UTC
04ccfc4 Don't prevent users to return a unit value in proc. [close #17227] 29 July 2015, 07:16 UTC
5945f0b 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 UTC
b0395bf clean up Hybrid theories (results are still the same modulo renaming of modules) 28 July 2015, 12:43 UTC
c2523f3 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 UTC
96e855d Remove unused `hypothesis` keyword. 28 July 2015, 09:43 UTC
61eb46a Extending base of results on last_ 28 July 2015, 08:41 UTC
daca4c9 Remove unused parse rules. 28 July 2015, 07:01 UTC
445abc1 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 UTC
c53f776 Define BigAlg as an exntesion of BigOp. 26 July 2015, 21:38 UTC
c6cf91d Add support for pattern (op-fix) in infix form. [fix #16786] 26 July 2015, 20:15 UTC
0a937a8 Add a exn. printer for lexical errors + improve lex error msgs. [fix #17223, #17224] 26 July 2015, 09:15 UTC
54fa7c1 Use alpha-eq. when searching for a contradiction in context. [close #17179] 25 July 2015, 09:55 UTC
8853bf3 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 UTC
49ffdf3 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 UTC
abed2a9 Better user error message when giving an invalid inv. to `call`. [fix #17110] 17 July 2015, 14:33 UTC
787e2ad In expressions (in proc.), give priority to program vars. [fix #17189] 17 July 2015, 10:46 UTC
80265d2 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 UTC
6336362 Detection of circular deps. [fix #17212] 17 July 2015, 09:28 UTC
f0c7ded Refactor-in printing functions. 17 July 2015, 07:39 UTC
f37ef90 Fix pretty-printing of oracle informations. [ref #17215] 14 July 2015, 15:44 UTC
9f6601d 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 UTC
25d7504 Pretty-printing of match-fix. [fix #17219] 12 July 2015, 12:14 UTC
9b8598c Set log-level to at least Warning when loading a theory. 12 July 2015, 12:14 UTC
52c261b 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 UTC
a56587b 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 UTC
8a89d9d Syntax change `lemma L : F by t` now takes a tactic sequence instead of a single tactic. [fix #17221] 12 July 2015, 12:13 UTC
ca59aac New reduction rule for equality over unit. `x = y --> true` when `x, y : unit`. 12 July 2015, 12:12 UTC
1a35e05 StdRing: nosmt. 10 July 2015, 20:30 UTC
e3f7ce1 Ring/Number: trivial lemmas. 10 July 2015, 20:13 UTC
d89a5af FSet: pick + trivial lemmas. 10 July 2015, 20:13 UTC
bdab7b1 Add some if-construct simplification lemmas. 10 July 2015, 20:13 UTC
536b08d finset: subset <-> card relation. 10 July 2015, 15:37 UTC
3282164 More facts on the zmodule op. 10 July 2015, 15:37 UTC
ce05b75 Remove reserved keywords from uniop 09 July 2015, 10:21 UTC
abf3561 Array: fix and prove make_append. 09 July 2015, 09:44 UTC
c61b653 NewFSet: core lemmas about cardinal. 07 July 2015, 14:32 UTC
880c7a0 Cleaning NewFSet a bit. 07 July 2015, 14:07 UTC
127bc94 Import basic theory of membership and finite sets. 07 July 2015, 13:37 UTC
back to top