| 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 |
| 483b80b | Pierre-Yves Strub | 07 July 2015, 13:15:04 UTC | Change notation for fset. | 07 July 2015, 13:15:04 UTC |
| c959352 | Pierre-Yves Strub | 07 July 2015, 10:54:55 UTC | New operator notation: ` opchar+ ` (where priority is taken from opchar+) | 07 July 2015, 13:14:54 UTC |
| 8102b1d | Benjamin Gregoire | 01 July 2015, 17:35:37 UTC | improve error message in cloning | 01 July 2015, 17:37:08 UTC |
| 8e1b50a | Benjamin Gregoire | 01 July 2015, 15:40:21 UTC | fix bug in cloning of operators | 01 July 2015, 15:40:41 UTC |
| 632b6bd | François Dupressoir | 30 June 2015, 10:02:33 UTC | Changes to PRF to clarify interfaces. This reverts commit 0a21f1da0c5fae4d3240b44a9838a2d71e8a75ff, which was itself a partial revert of its parent. | 30 June 2015, 10:03:13 UTC |
| 4acb16f | Pierre-Yves Strub | 29 June 2015, 15:40:57 UTC | bigops: replaced occurences of iota_ with range. | 29 June 2015, 15:40:57 UTC |
| 1e645ae | Pierre-Yves Strub | 29 June 2015, 15:38:13 UTC | Syntax lint. | 29 June 2015, 15:38:13 UTC |
| b3e1f6d | Pierre-Yves Strub | 26 June 2015, 15:23:27 UTC | Don't use ocamlbuild classical display on terminals. | 29 June 2015, 15:29:58 UTC |
| da354a5 | François Dupressoir | 29 June 2015, 13:37:07 UTC | ProofGeneral keywords. | 29 June 2015, 13:37:44 UTC |
| 377ffda | François Dupressoir | 29 June 2015, 13:36:22 UTC | Including .eca files in testsuites. Fixes #17216. | 29 June 2015, 13:37:44 UTC |
| b234fb8 | Benjamin Gregoire | 29 June 2015, 12:47:24 UTC | remove unused variable | 29 June 2015, 12:47:24 UTC |
| 8d17061 | Benjamin Gregoire | 29 June 2015, 12:31:05 UTC | remove one admit; add lemma | 29 June 2015, 12:31:05 UTC |
| 97ddba0 | Benjamin Gregoire | 29 June 2015, 08:12:15 UTC | add one missing lemma | 29 June 2015, 08:12:15 UTC |
| 6a8051e | Benjamin Gregoire | 28 June 2015, 16:58:41 UTC | instanciate ring tac for int | 28 June 2015, 16:58:41 UTC |
| 591aff2 | Pierre-Yves Strub | 28 June 2015, 16:18:42 UTC | Remove unused import. | 28 June 2015, 16:18:42 UTC |
| 963f9ee | Pierre-Yves Strub | 28 June 2015, 13:17:52 UTC | Libraries: axiom of choice (functional form). | 28 June 2015, 13:17:52 UTC |
| 9e4bb14 | François Dupressoir | 26 June 2015, 14:49:06 UTC | smt is finally useful! | 26 June 2015, 14:49:06 UTC |
| 3033738 | François Dupressoir | 26 June 2015, 14:40:31 UTC | Importing some missing definitions. | 26 June 2015, 14:40:31 UTC |
| a108f3f | Pierre-Yves Strub | 26 June 2015, 13:05:18 UTC | Removing remaining Why3 imports. | 26 June 2015, 14:11:53 UTC |
| 83cd782 | François Dupressoir | 26 June 2015, 13:01:03 UTC | Fixing the manual import, clarifying Euclidean Division. | 26 June 2015, 14:11:49 UTC |
| 7ae3d64 | François Dupressoir | 26 June 2015, 09:46:35 UTC | Replacing Why3 import with manual imports. Some remain in newth/NewIntCore.ec and newth/NewRealCore.ec. smt full and smt all currently fail for different reasons. | 26 June 2015, 14:11:43 UTC |
| 966282e | Pierre-Yves Strub | 26 June 2015, 08:20:50 UTC | Delete unused theory: map_why / intcore / realcore | 26 June 2015, 14:11:37 UTC |
| 6428569 | Pierre-Yves Strub | 25 June 2015, 19:09:17 UTC | Push core/hard-coded types/ops to a Pervasive theory. Conflicts: src/ec.ml Conflicts: src/ecScope.ml | 26 June 2015, 14:11:09 UTC |
| dfb2351 | Pierre-Yves Strub | 06 April 2015, 13:14:23 UTC | Remove old SMT interface & Why3 import The system is still unusable - its standard library as to be updated. Conflicts: src/ecEnv.ml src/ecEnv.mli src/ecHiGoal.ml src/ecHiGoal.mli src/ecHiTacticals.ml src/ecLowGoal.ml src/ecLowGoal.mli src/ecParser.mly src/ecParsetree.ml src/ecScope.ml src/why3/ecWhy3.ml src/why3/ecWhy3.mli | 26 June 2015, 14:08:10 UTC |
| 42d17e4 | Pierre-Yves Strub | 26 June 2015, 13:56:44 UTC | Recast low-level errors into user-local ones for `split`, `left` and `right`. [fix #17211] | 26 June 2015, 13:56:44 UTC |
| 6ff1147 | Pierre-Yves Strub | 26 June 2015, 12:36:09 UTC | `merlin` configuration file. | 26 June 2015, 12:36:09 UTC |
| a4bd813 | Pierre-Yves Strub | 26 June 2015, 11:17:40 UTC | Partially revert "Fix local variables names clash in pretty-printer" This reverts commit d643e6636f04f96ff5b5b93c1316e2587bac2ebd. [fix #17214] | 26 June 2015, 11:18:25 UTC |
| 47fa131 | Pierre-Yves Strub | 26 June 2015, 11:02:51 UTC | Right handling of paths when requir'ing theories from prelude. Conflicts: src/ecScope.ml | 26 June 2015, 11:05:28 UTC |
| c2bf74b | Pierre-Yves Strub | 26 June 2015, 07:38:28 UTC | Fix bug related to generation of fresh local hypotheses names. | 26 June 2015, 07:38:28 UTC |
| 843965e | Pierre-Yves Strub | 25 June 2015, 19:02:40 UTC | Remove wrongly committed files. | 25 June 2015, 19:02:40 UTC |
| 0cb0aaf | Pierre-Yves Strub | 25 June 2015, 14:51:26 UTC | Add `rewrite ... in ...` variant of `rewrite` Allows to use rewrite in hypotheses. The `in` only applies to the main goal (i.e. not to side goals). This construct is flagged as experimental. [fix #17208] | 25 June 2015, 15:04:58 UTC |
| 509fb50 | François Dupressoir | 25 June 2015, 10:23:57 UTC | Fixing the parts of the standard lib that can be fixed. | 25 June 2015, 10:23:57 UTC |
