| a6285ac | Benjamin Gregoire | 04 June 2014, 12:52:03 UTC | add base for rewrite | 04 June 2014, 12:52:03 UTC |
| d2afd01 | Pierre-Yves Strub | 04 June 2014, 09:49:10 UTC | autorewrite | 04 June 2014, 09:51:56 UTC |
| 3c9b043 | Francois Dupressoir | 29 May 2014, 06:45:01 UTC | Adding the OCaml patch to the MANIFEST. | 29 May 2014, 06:45:01 UTC |
| bbfb34f | Francois Dupressoir | 27 May 2014, 08:47:33 UTC | smt in some unit test. | 27 May 2014, 08:47:33 UTC |
| 323cb9e | Pierre-Yves Strub | 22 May 2014, 05:11:26 UTC | [case/elim] handle tuple. | 22 May 2014, 05:11:26 UTC |
| afe6f79 | Pierre-Yves Strub | 21 May 2014, 15:32:09 UTC | Better error message when case/elim is not applicable. | 21 May 2014, 15:32:09 UTC |
| 0eff9c7 | Pierre-Yves Strub | 21 May 2014, 15:22:14 UTC | [print glob] now works on module instantiations. | 21 May 2014, 15:22:14 UTC |
| d60ba6b | Pierre-Yves Strub | 21 May 2014, 15:12:10 UTC | Add a top level command for printing module globals Command is [print glob $mpath] | 21 May 2014, 15:12:10 UTC |
| 2231d00 | Pierre-Yves Strub | 20 May 2014, 14:41:43 UTC | Error messages for proof-terms application. | 20 May 2014, 14:41:43 UTC |
| d136561 | Pierre-Yves Strub | 20 May 2014, 14:17:48 UTC | Fix printing a tuple projections. | 20 May 2014, 14:17:48 UTC |
| 8da987c | Pierre-Yves Strub | 19 May 2014, 13:33:06 UTC | Internal refactoring: lexer can now return a list of lexems This should help better parsing operators. | 19 May 2014, 13:33:06 UTC |
| 677e0e3 | Pierre-Yves Strub | 19 May 2014, 12:41:35 UTC | [nosmt] for axiomatized operators. | 19 May 2014, 12:41:35 UTC |
| 754ddfd | Pierre-Yves Strub | 18 May 2014, 17:28:37 UTC | When in local mode, add the bin/ directory of the first toolchain to the system PATH. | 18 May 2014, 17:28:37 UTC |
| 8078c81 | Pierre-Yves Strub | 18 May 2014, 08:48:55 UTC | Update toolchain to OCaml 4.01 & Opam 1.1.0 Pactching OCaml s.t. it compiles on Mac. | 18 May 2014, 08:48:55 UTC |
| 041fd55 | Benjamin Gregoire | 16 May 2014, 14:50:10 UTC | instantiate hybrid with DDH | 16 May 2014, 14:50:10 UTC |
| da8f694 | Benjamin Gregoire | 16 May 2014, 13:45:21 UTC | Fix durty commit | 16 May 2014, 13:45:21 UTC |
| 136f660 | Benjamin Gregoire | 16 May 2014, 13:39:14 UTC | Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt/easycrypt into 1.0 | 16 May 2014, 13:39:14 UTC |
| 14a525f | Benjamin Gregoire | 16 May 2014, 13:39:00 UTC | more on hybrid | 16 May 2014, 13:39:00 UTC |
| 429ebad | Pierre-Yves Strub | 06 May 2014, 15:45:11 UTC | Remove staled roadmap - we have a web-based roadmap now. | 06 May 2014, 15:45:18 UTC |
| 281345d | Pierre-Yves Strub | 25 April 2014, 13:31:03 UTC | Fix test suite (rnd) | 25 April 2014, 13:31:03 UTC |
| 2220147 | Pierre-Yves Strub | 25 April 2014, 13:16:07 UTC | Fix capture of variables in substitution. | 25 April 2014, 13:16:07 UTC |
| 572c2ad | Pierre-Yves Strub | 25 April 2014, 13:01:04 UTC | Allow upper-case identifiers in [pose]. | 25 April 2014, 13:01:04 UTC |
| e6a7dec | Pierre-Yves Strub | 24 April 2014, 08:03:03 UTC | Factor code w.r.t the sections mechanism to its own module. | 24 April 2014, 14:52:17 UTC |
| 9c195bd | Francois Dupressoir | 24 April 2014, 12:38:14 UTC | Fixing examples after important bugfix. | 24 April 2014, 12:38:14 UTC |
| d024233 | Pierre-Yves Strub | 23 April 2014, 16:57:21 UTC | Fix f_andsa/f_orsa associativity | 23 April 2014, 16:57:21 UTC |
| a408a1d | Pierre-Yves Strub | 23 April 2014, 14:45:39 UTC | Fix error message in intro (was asserting false) | 23 April 2014, 14:45:39 UTC |
| 541ff05 | Pierre-Yves Strub | 23 April 2014, 09:57:20 UTC | Rework [rnd] tactic This fixes a bug in [rnd] when one of two distributions where empty. | 23 April 2014, 10:06:40 UTC |
| f16c9a3 | Francois Dupressoir | 10 April 2014, 21:09:46 UTC | Silencing LaTeX errors due to example obsolescence. | 10 April 2014, 21:09:46 UTC |
| 0bf9015 | Francois Dupressoir | 09 April 2014, 15:56:36 UTC | Stabilizing smt calls in PRG example. | 09 April 2014, 15:56:36 UTC |
| a6afa4f | Pierre-Yves Strub | 09 April 2014, 13:09:48 UTC | Why3 term alpha-convertibility + related maps refactored in [EcWhy3Conv]. | 09 April 2014, 13:09:48 UTC |
| 47b4be7 | Pierre-Yves Strub | 09 April 2014, 13:03:56 UTC | Why3 refactoring: subdirectory why3/ created and relevant files moved. | 09 April 2014, 13:03:56 UTC |
| 789a516 | Pierre-Yves Strub | 09 April 2014, 12:53:18 UTC | In [subst], don't clear a variable when it is defined. | 09 April 2014, 12:53:18 UTC |
| b7e75c7 | Pierre-Yves Strub | 09 April 2014, 12:31:54 UTC | Fix #17009 (better error messages) | 09 April 2014, 12:31:54 UTC |
| bdf003c | Francois Dupressoir | 08 April 2014, 14:22:30 UTC | Updating PRG example (some bad smt for some reason). | 08 April 2014, 14:22:30 UTC |
| fafd8fd | Francois Dupressoir | 08 April 2014, 14:07:42 UTC | Updating Plug_and_Pray. | 08 April 2014, 14:07:42 UTC |
| dff3779 | Pierre-Yves Strub | 08 April 2014, 12:23:19 UTC | Fix compilation issue with OCaml 4.00.x | 08 April 2014, 12:23:19 UTC |
| 6fe0ea9 | Pierre-Yves Strub | 07 April 2014, 14:29:35 UTC | Remove dead code form EcLogic/EcBaseLogic. | 07 April 2014, 14:29:35 UTC |
| 3423f87 | Pierre-Yves Strub | 12 March 2014, 17:48:52 UTC | Refactor all tactics using new proof engine. + disconnect type classes + reconnect legacy ring | 07 April 2014, 12:26:06 UTC |
| d4b1966 | Pierre-Yves Strub | 06 March 2014, 21:35:53 UTC | Split tacticals engine in its own module. | 04 April 2014, 13:22:40 UTC |
| ac5be62 | Pierre-Yves Strub | 06 March 2014, 21:09:25 UTC | Killed warnings (unused variables) | 04 April 2014, 13:22:40 UTC |
| 3206dfe | Francois Dupressoir | 03 April 2014, 10:21:21 UTC | Cleaning up the examples folder for distribution. | 03 April 2014, 10:21:25 UTC |
| 9c86b98 | Pierre-Yves Strub | 03 April 2014, 10:19:34 UTC | Add a global -timeout flag + timeout=0 => infinite timeout. | 03 April 2014, 10:19:34 UTC |
| 2cef9f2 | Francois Dupressoir | 01 April 2014, 17:40:53 UTC | Adding some useful axioms and lemmas on exponents. | 01 April 2014, 17:40:53 UTC |
| 8b15f74 | Benjamin Gregoire | 01 April 2014, 08:10:56 UTC | Add univ in AWord | 01 April 2014, 08:10:56 UTC |
| 6df81b6 | Benjamin Gregoire | 01 April 2014, 07:58:40 UTC | add product of two and 3 sets | 01 April 2014, 07:58:40 UTC |
| e43821c | Francois Dupressoir | 26 March 2014, 09:22:08 UTC | Reverting undesired changes to Means. The proofs are still broken, but they will at least work again when field and ring are fixed. | 26 March 2014, 09:22:08 UTC |
| ec6abbf | Francois Dupressoir | 25 March 2014, 21:51:20 UTC | I hate subdistributions. | 25 March 2014, 21:51:20 UTC |
| 45f3f0d | Francois Dupressoir | 25 March 2014, 13:52:42 UTC | A useful axiom on the unicity of the uniform distribution given a finite set. | 25 March 2014, 13:52:42 UTC |
| b2728cf | Francois Dupressoir | 24 March 2014, 11:27:03 UTC | ROM: Adding a useful initialization lemma. | 24 March 2014, 11:27:03 UTC |
| 70991a7 | Francois Dupressoir | 21 March 2014, 17:41:14 UTC | Fixing broken proof (ringeq). | 21 March 2014, 17:41:14 UTC |
| 6f77de0 | Francois Dupressoir | 21 March 2014, 17:36:58 UTC | Fixing a broken proof (broken fieldeq). | 21 March 2014, 17:36:58 UTC |
| 2aa700f | Francois Dupressoir | 21 March 2014, 17:28:39 UTC | ROM extended with some high-level transitions (up to collision on a given call, and abstract up to bad). Cleaning up examples directory. | 21 March 2014, 17:29:04 UTC |
| 9fc06a4 | Francois Dupressoir | 18 March 2014, 14:27:33 UTC | A generic-argument-based version of Hashed El Gamal -> CDH. | 18 March 2014, 14:27:33 UTC |
| 2271abe | Francois Dupressoir | 17 March 2014, 22:18:55 UTC | Hashed El Gamal ported over. No abstract proof steps. | 17 March 2014, 22:18:55 UTC |
| 555ded8 | Francois Dupressoir | 17 March 2014, 20:01:42 UTC | On the way to adapting Hashed El Gamal. CDH in 1.0, with bug workarounds galore! | 17 March 2014, 20:01:42 UTC |
| 1b2f432 | Francois Dupressoir | 11 March 2014, 08:53:31 UTC | Keywords | 11 March 2014, 08:53:31 UTC |
| 7b8628a | Pierre-Yves Strub | 06 March 2014, 21:06:04 UTC | Dead code removed ([claim]) | 06 March 2014, 21:06:04 UTC |
| 750bf41 | Pierre-Yves Strub | 06 March 2014, 21:00:20 UTC | Flow tcenv/tcenv1 types through the whole stack. A tactic is now a function from tcenv1 to tcenv. | 06 March 2014, 21:00:20 UTC |
| 10e469f | Pierre-Yves Strub | 05 March 2014, 09:15:45 UTC | Statically enforce that a goal has no subgoals. | 05 March 2014, 09:15:45 UTC |
| fe5a5ae | Pierre-Yves Strub | 04 March 2014, 15:19:43 UTC | Phl [fun] duplicated (old/new engine) | 04 March 2014, 15:19:43 UTC |
| cd9e600 | Pierre-Yves Strub | 04 March 2014, 15:11:24 UTC | Change type for external proof nodes: the list of depending proof handles is explicit. | 04 March 2014, 15:11:24 UTC |
| 8bf8166 | Pierre-Yves Strub | 04 March 2014, 08:58:17 UTC | Export more low-level elim. tactics of the new proof engine. | 04 March 2014, 08:58:17 UTC |
| 19bb8ea | Pierre-Yves Strub | 04 March 2014, 08:57:53 UTC | Parse-tree for [fun] related tactics factored. | 04 March 2014, 08:57:53 UTC |
| c2077f8 | Pierre-Yves Strub | 04 March 2014, 08:56:27 UTC | New accessors for proof environments. | 04 March 2014, 08:56:27 UTC |
| 3eecc72 | Pierre-Yves Strub | 04 March 2014, 08:53:35 UTC | conseq in new proof engine: module renaming. | 04 March 2014, 08:53:35 UTC |
| bc65216 | Pierre-Yves Strub | 03 March 2014, 16:57:08 UTC | Low level t_case in new proof engine. | 03 March 2014, 16:57:08 UTC |
| 341e546 | Pierre-Yves Strub | 03 March 2014, 16:40:53 UTC | Loew-level intro/elim in new engine. | 03 March 2014, 16:40:53 UTC |
| 5522365 | Pierre-Yves Strub | 03 March 2014, 09:32:38 UTC | In t_rewrite, check the proof term, even when the set of possible occurences is empty. | 03 March 2014, 09:32:38 UTC |
| 4d4a8b5 | Pierre-Yves Strub | 03 March 2014, 09:30:26 UTC | Low/Hi cut. | 03 March 2014, 09:30:26 UTC |
| d5a5f86 | Pierre-Yves Strub | 01 March 2014, 10:29:53 UTC | Fix of the proof for t_true. | 01 March 2014, 10:29:53 UTC |
| 804d3c6 | Pierre-Yves Strub | 28 February 2014, 20:40:09 UTC | Hi-level core rewriting in new proof engine. | 28 February 2014, 20:40:09 UTC |
| 41eef91 | Pierre-Yves Strub | 28 February 2014, 16:42:54 UTC | Low level rewrite in new proof-engine. | 28 February 2014, 16:42:54 UTC |
| 380d406 | Pierre-Yves Strub | 28 February 2014, 15:39:44 UTC | EcMetaProg -> EcMatching | 28 February 2014, 15:44:33 UTC |
| 434e522 | Pierre-Yves Strub | 28 February 2014, 15:38:59 UTC | Remove instruction pattern matching (dead code). | 28 February 2014, 15:38:59 UTC |
| 72d815a | Pierre-Yves Strub | 28 February 2014, 10:38:47 UTC | New engine refactored. | 28 February 2014, 10:38:47 UTC |
| 1eb3610 | Pierre-Yves Strub | 27 February 2014, 20:29:02 UTC | low/hi-level apply in new proof engine. | 27 February 2014, 20:29:02 UTC |
| 6010fad | Pierre-Yves Strub | 27 February 2014, 10:51:27 UTC | EcMetaProg.ml*: EOL whitespaces removed. | 27 February 2014, 10:51:27 UTC |
| fd69086 | Pierre-Yves Strub | 27 February 2014, 10:51:10 UTC | meta-prog: export core match function. | 27 February 2014, 10:51:10 UTC |
| d57a598 | Pierre-Yves Strub | 25 February 2014, 14:54:20 UTC | t_admit in new proof engine. | 25 February 2014, 14:54:20 UTC |
| 3ee806d | Pierre-Yves Strub | 25 February 2014, 14:31:23 UTC | Link proof <-> tcenv. | 25 February 2014, 14:31:23 UTC |
| e82dd33 | Pierre-Yves Strub | 25 February 2014, 11:48:42 UTC | Add entry points for the new proof-engine. | 25 February 2014, 11:56:20 UTC |
| 4dee4a4 | Pierre-Yves Strub | 24 February 2014, 15:07:08 UTC | More on the new proof-engine. Basic goals manipulation, including goal validation. | 24 February 2014, 15:07:08 UTC |
| 801b2e9 | Pierre-Yves Strub | 24 February 2014, 11:32:46 UTC | _tags: bin-annot + traverse only required structure. | 24 February 2014, 11:32:46 UTC |
| e8bfe27 | Francois Dupressoir | 21 February 2014, 16:53:56 UTC | Adding a useful lemma on swapping oget and omap. | 21 February 2014, 16:53:56 UTC |
| 0ccaa88 | Francois Dupressoir | 19 February 2014, 17:54:09 UTC | Exercise/Example: simulate a fair coin toss using only a coin of unknown bias p (p is neither 0 nor 1). To be finished. | 19 February 2014, 17:54:17 UTC |
| b526d53 | Pierre-Yves Strub | 19 February 2014, 17:02:59 UTC | Core API for the proof engine. | 19 February 2014, 17:02:59 UTC |
| af0428f | Benjamin Gregoire | 19 February 2014, 13:03:01 UTC | add tactic introsprogress | 19 February 2014, 13:03:12 UTC |
| 374fe1d | Benjamin Gregoire | 19 February 2014, 11:03:21 UTC | add lemma | 19 February 2014, 11:03:21 UTC |
| 8c9d5c9 | Benjamin Gregoire | 19 February 2014, 07:58:59 UTC | Fixing bug in fel. | 19 February 2014, 07:58:59 UTC |
| 77a4fe3 | Benjamin Gregoire | 18 February 2014, 16:24:05 UTC | Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt/easycrypt into 1.0 | 18 February 2014, 16:24:05 UTC |
| d1dd122 | Benjamin Gregoire | 18 February 2014, 16:21:17 UTC | add lemmas | 18 February 2014, 16:21:17 UTC |
| d19f056 | Pierre-Yves Strub | 16 February 2014, 18:09:50 UTC | In [kill] give at least 1 variable name that causes the failure. Fix #15949. | 16 February 2014, 18:09:50 UTC |
| a5330b0 | Pierre-Yves Strub | 16 February 2014, 17:17:31 UTC | When draining input stream, don't fail on lexical errors. Fix #16966. | 16 February 2014, 17:17:31 UTC |
| 044da6e | Francois Dupressoir | 14 February 2014, 11:35:51 UTC | Fixing a bug on bdHoare while rule. cherry-picked from Cesar's master commit. | 14 February 2014, 11:35:51 UTC |
| bd6886c | Francois Dupressoir | 12 February 2014, 11:51:52 UTC | Fun with globs: a generic proof of the fundamental lemma. | 12 February 2014, 11:51:52 UTC |
| a82d6f3 | Pierre-Yves Strub | 11 February 2014, 22:11:44 UTC | Don't try to select type-class operators when non-tc operators are selectable. | 11 February 2014, 22:11:44 UTC |
| d2ad733 | Pierre-Yves Strub | 11 February 2014, 21:54:17 UTC | Merge branch 'master' into 1.0 Conflicts: src/ecFol.ml src/ecParser.mly src/ecParsetree.ml src/ecPrinting.ml tests/phl/success/0005-sp-2.ec tests/phl/success/0005-sp.ec theories/FMap.ec | 11 February 2014, 21:57:14 UTC |
| 3ae04fb | Pierre-Yves Strub | 11 February 2014, 21:42:46 UTC | Kill warnings. | 11 February 2014, 21:42:46 UTC |
| 413ee91 | Pierre-Yves Strub | 10 February 2014, 16:22:13 UTC | Script for stripping comments | 10 February 2014, 16:22:29 UTC |
| ed22d75 | Francois Dupressoir | 10 February 2014, 10:50:54 UTC | Dice_sampling.ec: very minor cleanup. | 10 February 2014, 10:50:54 UTC |
