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 |