| 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 |
| 1e906b8 | François Dupressoir | 25 May 2015, 10:12:47 UTC | Only NewMap fails as a reminder that it needs to be fixed. | 25 May 2015, 10:12:47 UTC |
| 904f418 | François Dupressoir | 25 May 2015, 09:43:12 UTC | Fun.ec: eta f = f non-extensional. | 25 May 2015, 09:43:12 UTC |
| d7b985a | François Dupressoir | 11 May 2015, 14:26:38 UTC | Pushing distributions out of datatypes. Adding some useful predicates on distr. | 25 May 2015, 09:04:53 UTC |
| 39da530 | François Dupressoir | 11 May 2015, 10:49:18 UTC | Draft theories for Symmetric Key Encryption theories. | 25 May 2015, 09:04:53 UTC |
| 225cef7 | François Dupressoir | 08 May 2015, 15:50:52 UTC | First attempt at organizing the crypto libraries a bit better. | 25 May 2015, 09:04:53 UTC |
| ae51936 | François Dupressoir | 08 May 2015, 14:12:40 UTC | End of cherry-picking. | 25 May 2015, 09:03:51 UTC |
| d82951c | François Dupressoir | 08 May 2015, 13:44:27 UTC | Adding useful lemmas about head and behead. | 25 May 2015, 09:00:58 UTC |
| b28cb2e | François Dupressoir | 08 May 2015, 12:01:09 UTC | Minor cleanup in core libs. Conflicts: theories/newth/NewList.ec | 25 May 2015, 09:00:58 UTC |
| 1c63c99 | François Dupressoir | 08 May 2015, 09:37:00 UTC | Minor on Fun.ec | 25 May 2015, 09:00:58 UTC |
| 53156c9 | François Dupressoir | 21 April 2015, 13:58:41 UTC | Pred.ec to follow ssrbool more closely. Adapting other theories. | 25 May 2015, 09:00:58 UTC |
| be4b8fa | François Dupressoir | 21 April 2015, 13:33:23 UTC | NewLogic. | 25 May 2015, 09:00:58 UTC |
| feefc9f | Pierre-Yves Strub | 24 May 2015, 19:44:19 UTC | Documentation is now externalized See: https://github.com/EasyCrypt/easycrypt-doc | 24 May 2015, 19:44:19 UTC |
| 409993e | François Dupressoir | 21 May 2015, 21:25:35 UTC | Attempt at pushing better-structured libs through for the school. | 21 May 2015, 21:25:35 UTC |
| b834e00 | François Dupressoir | 21 May 2015, 15:18:23 UTC | Merging smt branch and fixing libs as much as possible. | 21 May 2015, 15:18:23 UTC |
| 5b52216 | Pierre-Yves Strub | 14 May 2015, 15:25:28 UTC | Remove unused webui terminal. | 14 May 2015, 15:25:28 UTC |
| 0008cf8 | Pierre-Yves Strub | 14 May 2015, 14:32:33 UTC | Remove staled UI file, keeping emacs-based packaging scripts. See easycrypt-atom mode. | 14 May 2015, 14:32:33 UTC |
| ffbd218 | Pierre-Yves Strub | 12 May 2015, 15:17:06 UTC | Fix compilation issues. | 12 May 2015, 15:17:06 UTC |
| aa2f1c6 | Pierre-Yves Strub | 28 April 2015, 15:03:46 UTC | Extend conversion with path normalisation. Conflicts: src/ecReduction.ml | 12 May 2015, 19:59:10 UTC |
| 538ad78 | Pierre-Yves Strub | 08 May 2015, 15:50:00 UTC | README.md Wodi has been disbanded. | 08 May 2015, 15:50:00 UTC |
| 26db9a3 | Pierre-Yves Strub | 05 May 2015, 09:45:31 UTC | ZModP: normalized names. | 05 May 2015, 09:45:31 UTC |
| abd634b | Pierre-Yves Strub | 05 May 2015, 09:42:14 UTC | Some results from the arithmetica project. | 05 May 2015, 09:42:14 UTC |
| c942f46 | Benjamin Gregoire | 02 May 2015, 07:38:12 UTC | Fix bug, should be ported in other branches | 02 May 2015, 07:38:34 UTC |
| abfa9a5 | Pierre-Yves Strub | 30 April 2015, 19:51:56 UTC | Fix MANIFEST | 30 April 2015, 19:51:56 UTC |
| 016ff7e | Pierre-Yves Strub | 30 April 2015, 17:04:51 UTC | keywords generator: support for atom cson file format. | 30 April 2015, 17:05:07 UTC |
| c6a7922 | Pierre-Yves Strub | 30 April 2015, 16:45:59 UTC | Remove staled script for src2src transformation. | 30 April 2015, 17:05:05 UTC |
| 85d07a3 | Pierre-Yves Strub | 30 April 2015, 13:30:24 UTC | README | 30 April 2015, 13:30:24 UTC |
| a70c27f | Pierre-Yves Strub | 30 April 2015, 13:17:53 UTC | Update README + scripts for using github opam repo. | 30 April 2015, 13:17:53 UTC |
| 7c4ae73 | Pierre-Yves Strub | 30 April 2015, 12:08:29 UTC | Force markdown for the README file. | 30 April 2015, 12:08:44 UTC |
| 0568ff0 | François Dupressoir | 20 April 2015, 08:12:33 UTC | Adding filter to FSet. | 20 April 2015, 08:12:33 UTC |
| 2a273fb | François Dupressoir | 17 April 2015, 09:24:11 UTC | Drafts for string and word theories. | 17 April 2015, 10:04:44 UTC |
| 4627e81 | François Dupressoir | 17 April 2015, 08:09:17 UTC | NewFSet -> small things. | 17 April 2015, 08:09:17 UTC |
| 95b590a | Pierre-Yves Strub | 09 April 2015, 07:12:38 UTC | .gitignore | 13 April 2015, 13:58:03 UTC |
| 6b42213 | François Dupressoir | 13 April 2015, 13:37:36 UTC | NewFMap should export Option and NewFSet. | 13 April 2015, 13:37:36 UTC |
| eaf99e9 | Benjamin Gregoire | 13 April 2015, 11:40:07 UTC | small fix | 13 April 2015, 11:40:07 UTC |
| db6b94f | Benjamin Gregoire | 13 April 2015, 10:47:31 UTC | add few lemmas in BigOp | 13 April 2015, 10:47:31 UTC |
| 7b7ce3c | Benjamin Gregoire | 12 April 2015, 06:24:01 UTC | improve option selection | 12 April 2015, 06:24:01 UTC |
| fd08665 | Benjamin Gregoire | 10 April 2015, 13:14:24 UTC | improve smt. | 10 April 2015, 13:14:40 UTC |
| f639006 | François Dupressoir | 10 April 2015, 10:36:40 UTC | Cleaning up smt documentation. | 10 April 2015, 10:36:40 UTC |
| abad2eb | Benjamin Gregoire | 09 April 2015, 19:19:38 UTC | doc of smt :-) | 09 April 2015, 19:19:38 UTC |
| 1fad64f | Benjamin Gregoire | 09 April 2015, 19:19:18 UTC | minor change | 09 April 2015, 19:19:18 UTC |
| 53761ab | Benjamin Gregoire | 09 April 2015, 16:59:03 UTC | add why3 translation of let on record | 09 April 2015, 16:59:03 UTC |
| 5ede6c9 | Benjamin Gregoire | 09 April 2015, 16:10:26 UTC | simplify traduction of tuple and projection | 09 April 2015, 16:10:26 UTC |
| 798001b | Benjamin Gregoire | 09 April 2015, 14:01:27 UTC | just to try | 09 April 2015, 14:01:27 UTC |
| 08820d4 | Benjamin Gregoire | 09 April 2015, 14:01:15 UTC | fix bug | 09 April 2015, 14:01:15 UTC |
| ccbc3f4 | Benjamin Gregoire | 09 April 2015, 13:30:56 UTC | fix stuff | 09 April 2015, 13:30:56 UTC |
| b535568 | Benjamin Gregoire | 09 April 2015, 12:41:48 UTC | add iterated version of hypothesis selection | 09 April 2015, 12:41:48 UTC |
| 1514f92 | François Dupressoir | 09 April 2015, 09:14:41 UTC | Abstract theories are abstract. | 09 April 2015, 09:14:41 UTC |
| 4d7001e | Benjamin Gregoire | 09 April 2015, 08:28:50 UTC | improve syntax, start to add more option | 09 April 2015, 08:28:50 UTC |
| 5b499dc | Benjamin Gregoire | 08 April 2015, 23:48:02 UTC | improve use of options in ecSmt. The selection of axioms is now based also on operators used inside operators ... | 08 April 2015, 23:48:02 UTC |
| 12cd0be | Benjamin Gregoire | 08 April 2015, 23:46:15 UTC | fix bug in translation of constructor | 08 April 2015, 23:46:15 UTC |
| 22af791 | Benjamin Gregoire | 08 April 2015, 23:45:41 UTC | add iterator over axiom | 08 April 2015, 23:45:41 UTC |
| 49f74c6 | Benjamin Gregoire | 08 April 2015, 19:42:24 UTC | small refactoring | 08 April 2015, 19:42:24 UTC |
| 2f7e73a | Benjamin Gregoire | 08 April 2015, 19:38:08 UTC | add possibility to write cut := (l x). | 08 April 2015, 19:38:08 UTC |
| 321afae | Benjamin Gregoire | 08 April 2015, 18:05:43 UTC | add printing option in smt | 08 April 2015, 18:05:43 UTC |
| 5e741db | Benjamin Gregoire | 08 April 2015, 18:05:26 UTC | fix bug in translation of fix point | 08 April 2015, 18:05:26 UTC |
| e2c2299 | Benjamin Gregoire | 08 April 2015, 16:37:32 UTC | add more option to smt | 08 April 2015, 16:37:32 UTC |
| 0533762 | Benjamin Gregoire | 02 April 2015, 15:02:18 UTC | modify axiom selection | 07 April 2015, 13:02:52 UTC |
