| 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 |
| 635e8fc | François Dupressoir | 25 June 2015, 09:41:38 UTC | PRP: adding a layer of abstraction to allow better black-box use. | 25 June 2015, 09:41:43 UTC |
| 8cc9bfd | Pierre-Yves Strub | 24 June 2015, 21:08:24 UTC | Library: lists: linking mem / nth. | 24 June 2015, 21:08:24 UTC |
| 2acc520 | Pierre-Yves Strub | 23 June 2015, 20:21:18 UTC | refactoring: factor out part of NewDistr. New modules are: - RealExtra: axiomatization of the real lub - RealSeq: real sequence - RealSeries: real series | 24 June 2015, 14:09:26 UTC |
| 1ea87c6 | Pierre-Yves Strub | 24 June 2015, 13:06:37 UTC | real/int ordering subsumed by core number theory. | 24 June 2015, 13:07:20 UTC |
| 6f8f464 | Pierre-Yves Strub | 24 June 2015, 10:47:41 UTC | Equip `real` with its field structure. | 24 June 2015, 10:48:10 UTC |
| c876f84 | Pierre-Yves Strub | 24 June 2015, 10:47:23 UTC | Add missing copyrights + cleaning spacing. | 24 June 2015, 10:48:00 UTC |
| 017e0c6 | Pierre-Yves Strub | 24 June 2015, 10:16:30 UTC | Remove hard-coded tuple induction principles. | 24 June 2015, 10:16:36 UTC |
| 831440a | Pierre-Yves Strub | 24 June 2015, 10:14:31 UTC | prelude: temporary operators reflecting forall/exists. Should be removed when #17209 is fixed. | 24 June 2015, 10:14:57 UTC |
| f37283a | Pierre-Yves Strub | 24 June 2015, 10:09:45 UTC | Library: lists: extra lemmas on `rem`. | 24 June 2015, 10:10:48 UTC |
| 13c9d73 | François Dupressoir | 24 June 2015, 09:37:28 UTC | PRP theory now takes the inverse permutation as parameter. Also added security notion for Strong PRP, and generic result that every Strong PRP is a PRP. | 24 June 2015, 09:37:36 UTC |
| e2b0c63 | Pierre-Yves Strub | 23 June 2015, 12:55:19 UTC | pretty-printer: bug fix. Fix missing parentheses around anonymous proc. argument types. [fix #17206] | 23 June 2015, 12:55:19 UTC |
| 4a91204 | Pierre-Yves Strub | 23 June 2015, 12:15:00 UTC | Libraries: more on distribution (std. def.) | 23 June 2015, 12:15:00 UTC |
| 078b2cf | Pierre-Yves Strub | 22 June 2015, 14:34:26 UTC | Axiomatizing the def. of pr(E). | 22 June 2015, 14:34:34 UTC |
| ad4f41a | François Dupressoir | 22 June 2015, 12:15:24 UTC | Cleaning up new version of ditributions on sets (form only). | 22 June 2015, 12:15:24 UTC |
| 4ff282c | François Dupressoir | 22 June 2015, 11:15:43 UTC | [Libraries] Only remaining instances of 'smt full' are those that do not go through with 'smt all'. Note that NewRealOrder.ec also has some admits that have been tagged as issues with the SMT-LIB connections by whoever. | 22 June 2015, 11:15:43 UTC |
| 2d69fa5 | Pierre-Yves Strub | 19 June 2015, 17:38:06 UTC | In proc., it is not mandatory anymore to store the result of a procedure call. [close #17204] | 19 June 2015, 17:38:06 UTC |
| aa34347 | Pierre-Yves Strub | 19 June 2015, 16:14:57 UTC | parser: support for new syntax for assignments in var. declarations [fix #17205] | 19 June 2015, 16:14:57 UTC |
| 67310f9 | François Dupressoir | 19 June 2015, 15:34:19 UTC | [Libraries] Minor. | 19 June 2015, 15:34:23 UTC |
| 986f706 | Pierre-Yves Strub | 17 June 2015, 14:15:49 UTC | In pattern-matching: restore old unification state on failure. [fix #17198] | 17 June 2015, 14:15:49 UTC |
| 78a119c | Pierre-Yves Strub | 17 June 2015, 14:14:56 UTC | pretty-printer (bis): use new notations (<-, <$, <@) everywhere. | 17 June 2015, 14:14:56 UTC |
| f00796d | Pierre-Yves Strub | 17 June 2015, 14:04:44 UTC | pretty-printer: use new notations (<-, <$, <@) everywhere. | 17 June 2015, 14:04:44 UTC |
| a2dc86c | Pierre-Yves Strub | 17 June 2015, 13:22:00 UTC | Fix bugs related to operators renaming in NewDistr. | 17 June 2015, 13:22:25 UTC |
| d7a5d9d | Pierre-Yves Strub | 17 June 2015, 13:21:48 UTC | Fix shadowing in pretty-printer of global op/pred names. When an operator/predicate name is shadowed by a local variable, do pretty-print a qualified name to disambiguate the resolution. This patch also add some debug functions for printing type variables instances of operators/predicates. [fix #17203] | 17 June 2015, 13:21:48 UTC |
| db61759 | Pierre-Yves Strub | 17 June 2015, 09:06:28 UTC | Some facts about big summation (in a group) | 17 June 2015, 09:06:28 UTC |
| e671281 | Pierre-Yves Strub | 17 June 2015, 06:20:33 UTC | Bigop: merge + nosmt + renaming - merge old BigOp theory (old theory deleted) - add `nosmt` to nearly all bigops lemmas - rename `big_nat_*` to `big_int_*` | 17 June 2015, 06:20:53 UTC |
