| 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 |
| a2e8318 | Pierre-Yves Strub | 07 April 2015, 12:50:25 UTC | Fix subtype + parsing of unary operators. | 07 April 2015, 12:50:25 UTC |
| cbda3e4 | Pierre-Yves Strub | 07 April 2015, 12:25:38 UTC | Internal: refactoring of operators lexing. This refactoring should lead to a mode where tacticals notations like `[->|]` should not fail anymore. This commit is also on the path to give users the ability to declare operators at a given associativity and precedence level. The current state of operators lexing is unstable. | 07 April 2015, 12:25:52 UTC |
| 4e1ff40 | Pierre-Yves Strub | 06 April 2015, 12:39:31 UTC | Smt: translation of fixpoints + some refactoring. | 06 April 2015, 12:39:31 UTC |
| 74ca476 | Pierre-Yves Strub | 23 March 2015, 16:06:32 UTC | SAT traces only generated on demand SAT traces are only generated when the env. variables EC_SMT_DEBUG is set. | 06 April 2015, 10:15:56 UTC |
| c1a0c15 | Pierre-Yves Strub | 02 April 2015, 16:14:28 UTC | Remove staled 'roadmap' files. | 02 April 2015, 16:14:28 UTC |
| de5946b | Pierre-Yves Strub | 01 April 2015, 10:21:19 UTC | Some progress on IntDiv. | 01 April 2015, 10:21:19 UTC |
| 2616382 | Pierre-Yves Strub | 01 April 2015, 10:21:13 UTC | Applicative view. `move/(_ x1 ... xn)` now stands for the applicative view. The top-assumption is applied to the arguments `x1 ... xn`. | 01 April 2015, 10:21:13 UTC |
| ce62fe4 | François Dupressoir | 25 March 2015, 07:46:27 UTC | Stub for Why3 maps. | 25 March 2015, 07:46:27 UTC |
| 9df6300 | Benjamin Gregoire | 24 March 2015, 15:52:11 UTC | fix bug | 24 March 2015, 15:55:15 UTC |
| 618f80e | Pierre-Yves Strub | 24 March 2015, 15:21:05 UTC | SMT: Commit current state about fixpoints + refactoring | 24 March 2015, 15:21:05 UTC |
| d5cd488 | Pierre-Yves Strub | 23 March 2015, 16:06:32 UTC | SAT traces only generated on demand SAT traces are only generated when the env. variables EC_SMT_DEBUG is set. | 23 March 2015, 16:06:32 UTC |
| 8f803c0 | Pierre-Yves Strub | 23 March 2015, 15:55:52 UTC | License update: standard library moved from CeCILL-C to CeCILL-B This allows the non-contagion of user developments. The EasyCrypt engine stays in CeCILL-C. | 23 March 2015, 15:55:52 UTC |
| 9d1b03a | Pierre-Yves Strub | 23 March 2015, 15:44:14 UTC | Push a large chunk of wanted lemmas about real intergral domains. | 23 March 2015, 15:44:14 UTC |
| 1430f7f | Pierre-Yves Strub | 23 March 2015, 13:18:08 UTC | Specification of euclidean division. | 23 March 2015, 15:28:22 UTC |
| f08556d | Benjamin Gregoire | 23 March 2015, 13:06:00 UTC | SMT: axiom selection | 23 March 2015, 13:35:42 UTC |
| 97a86ba | Benjamin Gregoire | 13 March 2015, 20:50:46 UTC | add pvar glob tglob and Pr translations + fix bug + refactoring. | 23 March 2015, 13:30:48 UTC |
| 7585325 | Pierre-Yves Strub | 22 March 2015, 15:07:25 UTC | Fix `catch` clause not catching the right exception [fix #17187]: anomaly when invalid memory is referenced | 22 March 2015, 15:07:25 UTC |
| 41f0016 | Pierre-Yves Strub | 10 March 2015, 14:28:05 UTC | New SMT tactic. This commit brings a new `smt` tactic that can be called via `smt:lazy`. This tactic relies on a lazy translation of operators/lemmas and is currently missing: - a proper selection of lemmas to sent - the translation of body of fixpoints - a set of flags to better control the translation (including the use of the already existing hints databases) The default `smt` version to be called can be controlled via the `Smt:lazy` option. By default, the legacy version is used. If changed to the new one, the old one can be locally called via the `smt:full` variant of `smt`. This commit also bring a `time` meta command that can be used to time any vernacular command by simply executing: `time thecommand.` | 20 March 2015, 15:44:19 UTC |
| 39d4a0b | Pierre-Yves Strub | 18 March 2015, 23:16:01 UTC | Add a report URL. [fix #17185] | 18 March 2015, 23:16:01 UTC |
| 2fbf6c7 | François Dupressoir | 16 March 2015, 13:43:38 UTC | Doc: adding 'have', some minor things in other tactics. | 16 March 2015, 13:43:38 UTC |
| 4797bab | François Dupressoir | 16 March 2015, 12:06:37 UTC | Folding array notations into NewList.Array. | 16 March 2015, 12:06:37 UTC |
