| 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 |
| 64b8cb9 | Pierre-Yves Strub | 17 June 2015, 05:56:27 UTC | [rewrite]: all global symbols now act as a rewrite base. The rewrite base of the qsymbol `p` is composed of all accessible lemmas that `p` resolves to. | 17 June 2015, 05:56:44 UTC |
| 68f9520 | Pierre-Yves Strub | 16 June 2015, 19:38:28 UTC | New syntax for assignment / sampling / procedure call. Following Alley's idea: * `x <- e` stands for assigning the expression `e` in the left-value `x` * 'x <$ e` stands for assigning the result of sampling from the distribution expression `e` in the left-value `x` * 'x <@ X.f()` stands for assigning the result of the procedure call `X.f()` to the left-value `x` The old syntax (`x = e`, `x = $e`, `x = X.f()` when `X.f()` does not contain functor applications are still active. However, the pretty-printer makes use of the new notation. The unused syntax `x <- X.f()` has been removed. [fix #17184] | 16 June 2015, 19:38:44 UTC |
| 45ca71a | Benjamin Gregoire | 16 June 2015, 14:49:17 UTC | instantiate bigop with standard operators | 16 June 2015, 14:49:36 UTC |
| d334eb3 | Pierre-Yves Strub | 16 June 2015, 10:03:42 UTC | Localization of errors encoutered in required libraries. [fix #17200] | 16 June 2015, 10:03:42 UTC |
| c11fdd2 | Pierre-Yves Strub | 16 June 2015, 09:11:08 UTC | Low intro: do nothing is list of ids is empty. | 16 June 2015, 09:12:32 UTC |
| aeae276 | Pierre-Yves Strub | 16 June 2015, 08:34:57 UTC | Weak form of keyed macthing. | 16 June 2015, 08:34:57 UTC |
| e5933e9 | Pierre-Yves Strub | 15 June 2015, 21:06:22 UTC | PG: when no prompt is avail., should assume that weak-check is not enabled. [fix #17199] | 15 June 2015, 21:06:22 UTC |
| c011738 | Pierre-Yves Strub | 15 June 2015, 20:52:11 UTC | Refactor integer intervals theory + proofs. | 15 June 2015, 20:52:11 UTC |
| a79efa9 | Pierre-Yves Strub | 15 June 2015, 15:07:18 UTC | bigop: new properties about big/Z (assuming a theory of integer intervals) | 15 June 2015, 15:37:23 UTC |
| 6fa3c4a | Benjamin Gregoire | 15 June 2015, 14:41:18 UTC | add eta in conversion | 15 June 2015, 14:41:34 UTC |
| ec0fce2 | Pierre-Yves Strub | 15 June 2015, 14:29:48 UTC | newBigop: use new Pred.ec notations. | 15 June 2015, 14:29:48 UTC |
| 417d315 | Pierre-Yves Strub | 15 June 2015, 13:42:25 UTC | newBigop: extra properties. | 15 June 2015, 13:42:25 UTC |
| 618d5eb | Pierre-Yves Strub | 15 June 2015, 13:33:05 UTC | newBigop: extra properties. | 15 June 2015, 13:35:40 UTC |
| cf8b4bd | Pierre-Yves Strub | 15 June 2015, 12:48:08 UTC | newBigop: operator renaming: `sum` -> `big` Conflicts: theories/newth/NewBigop.eca | 15 June 2015, 13:35:35 UTC |
| 73c9fe3 | Pierre-Yves Strub | 15 June 2015, 12:40:35 UTC | newList: more properties on `iota_` | 15 June 2015, 13:34:23 UTC |
| d643e66 | Pierre-Yves Strub | 15 June 2015, 12:18:45 UTC | Fix local variables names clash in pretty-printer 1. the bound memory appearing Pr[] is now treated correctly 2. is a local name ends with a digit, add a '_' between the name and the numerical postfix added by the printer. [fix #17186] | 15 June 2015, 12:18:45 UTC |
| 2605d84 | Pierre-Yves Strub | 15 June 2015, 11:20:23 UTC | Fix pretty-printing of lists. List literals are now correctly printed as `[x1; ...; xn]`. [fix #17097] | 15 June 2015, 11:20:23 UTC |
| f963dc2 | Pierre-Yves Strub | 15 June 2015, 09:46:21 UTC | Bad error message in wrongly applied view. Fail gracefully when all type variables of a view cannot be inferred from its application constraints. [fix #17177] | 15 June 2015, 09:46:21 UTC |
| f55f76c | Pierre-Yves Strub | 15 June 2015, 09:42:11 UTC | Fix compilation issue (wrong rule name in parser) | 15 June 2015, 09:42:11 UTC |
| c5242d4 | Pierre-Yves Strub | 15 June 2015, 07:32:25 UTC | Fix reduce/reduce conflicts in parser. The previous intended grammar for SMT options was genuinely ambiguous and had to be changed. `dbhints` lists (when # > 1) have to be parenthesized, i.e.: `smt wanted=@T` but `smt wanted=(@T -T.l)` | 15 June 2015, 07:32:25 UTC |
| eef3347 | Pierre-Yves Strub | 14 June 2015, 21:19:03 UTC | Refactor SMT options parsing. In prevision of generalizing the mechanism for other tactics. | 14 June 2015, 21:19:03 UTC |
| 5a1bb86 | Pierre-Yves Strub | 14 June 2015, 21:18:45 UTC | ecSmt: core operators: use type-safe cast. | 14 June 2015, 21:18:45 UTC |
| 5e00b90 | Pierre-Yves Strub | 14 June 2015, 18:21:27 UTC | ecReduction: dead code removal. | 14 June 2015, 18:21:27 UTC |
| c0060ae | Pierre-Yves Strub | 14 June 2015, 16:40:38 UTC | When genralizing a symbol, don't always use its name for creating idents. In case the generalized symbol is a special symbol ([], [_<-_], ...), create a symbol based on its type name. [fix #17178] | 14 June 2015, 16:40:38 UTC |
| 5d50460 | Pierre-Yves Strub | 14 June 2015, 16:25:35 UTC | EcSmt: Cast (to prop) arguments of internal boolean operators [fix #17193] | 14 June 2015, 16:25:48 UTC |
| e68d4ff | Pierre-Yves Strub | 13 June 2015, 14:01:51 UTC | Change behaviour of [progress] [progress] is now trying to close final goal with [trivial], i.e. is equivalent to [old:progress=> //]. [fix #17190] | 13 June 2015, 14:01:51 UTC |
| 229d8f4 | Pierre-Yves Strub | 12 June 2015, 16:01:36 UTC | In pattern matching, always executing default conv. check on failure. | 12 June 2015, 16:01:36 UTC |
| 171085f | Pierre-Yves Strub | 12 June 2015, 15:40:04 UTC | Remove dead code. | 12 June 2015, 15:40:04 UTC |
| d5e8952 | Pierre-Yves Strub | 12 June 2015, 15:04:13 UTC | Test file for higher-order pattern matching (imitation). | 12 June 2015, 15:04:13 UTC |
| c3dd2a9 | Pierre-Yves Strub | 12 June 2015, 15:02:11 UTC | Ecmathcing: support HO-imitation like patterns. | 12 June 2015, 15:02:11 UTC |
| a66293e | Pierre-Yves Strub | 12 June 2015, 13:43:18 UTC | In pattern matching, reduce head beta-redexes when matching fails. | 12 June 2015, 13:43:18 UTC |
| b59d31a | Alley Stoughton | 03 June 2015, 20:46:39 UTC | Merge branch '1.0' of github.com:EasyCrypt/easycrypt into 1.0 | 03 June 2015, 20:46:39 UTC |
| 4ba4692 | Alley Stoughton | 03 June 2015, 20:46:10 UTC | Version of br93 that came out of US school. | 03 June 2015, 20:46:10 UTC |
| 440f7e3 | Pierre-Yves Strub | 31 May 2015, 17:07:00 UTC | Packaging: script for macos | 31 May 2015, 17:10:48 UTC |
| 171d229 | Pierre-Yves Strub | 30 May 2015, 17:35:31 UTC | Add an environment variable for dumping Why3 tasks. | 30 May 2015, 17:35:31 UTC |
| 2d58336 | Pierre-Yves Strub | 30 May 2015, 17:29:55 UTC | SMT: clean up dead code, use notifier for notifications. | 30 May 2015, 17:29:55 UTC |
| 1a4d7b4 | Pierre-Yves Strub | 28 May 2015, 11:27:40 UTC | packaging: automatization of binary packages for linux platforms. | 28 May 2015, 11:27:40 UTC |
| 7493d5e | Pierre-Yves Strub | 27 May 2015, 10:47:24 UTC | emacs-based packages: update why3.conf | 27 May 2015, 10:47:24 UTC |
| 21db6da | François Dupressoir | 26 May 2015, 13:11:59 UTC | Updating some examples. | 26 May 2015, 13:11:59 UTC |
| 2ea9e0a | François Dupressoir | 26 May 2015, 12:50:53 UTC | Birthday bound revisited. | 26 May 2015, 12:50:53 UTC |
| 8c21c72 | François Dupressoir | 25 May 2015, 15:57:49 UTC | Making PRF use new notations for properties of distributions. | 25 May 2015, 15:57:49 UTC |
| 6926bb2 | François Dupressoir | 25 May 2015, 15:44:43 UTC | PRG is an abstract theory. | 25 May 2015, 15:44:43 UTC |
| ccd6418 | François Dupressoir | 25 May 2015, 15:16:10 UTC | Modify MANIFEST: no more doc. | 25 May 2015, 15:16:10 UTC |
