| 00cc7d0 | Benjamin Gregoire | 28 July 2017, 04:19:44 UTC | intermediary stuff | 28 July 2017, 09:58:12 UTC |
| 13e9173 | Pierre-Yves Strub | 27 July 2017, 06:23:30 UTC | Check validity of obtained named from a theory cloning renaming. [fix #17354] | 27 July 2017, 06:23:37 UTC |
| 058bd27 | Pierre-Yves Strub | 27 July 2017, 06:05:52 UTC | Fix bug in pretty printer. Fix printing of higher-order notation (not in eta-normal form). [fix #17355] | 27 July 2017, 06:05:52 UTC |
| 0c50716 | François Dupressoir | 25 July 2017, 17:12:23 UTC | Lining definitions up for OAEP. | 25 July 2017, 17:16:19 UTC |
| b4c2a37 | Benjamin Gregoire | 24 July 2017, 17:18:07 UTC | bound the probability that an adversary distinguish between the oracle x <@ d \ X and x <@ d | 24 July 2017, 17:18:23 UTC |
| e401883 | Benjamin Gregoire | 24 July 2017, 17:16:15 UTC | more info when local lemma fail. | 24 July 2017, 17:18:23 UTC |
| ddf604b | François Dupressoir | 24 July 2017, 17:17:56 UTC | Fixing vonNeumann | 24 July 2017, 17:17:56 UTC |
| f173dc4 | François Dupressoir | 24 July 2017, 17:15:18 UTC | "Fixing" PRP<->PRF lemmas | 24 July 2017, 17:15:18 UTC |
| e456402 | Benjamin Gregoire | 21 July 2017, 13:32:24 UTC | fix some theories | 21 July 2017, 13:32:33 UTC |
| 3e10ebb | Benjamin Gregoire | 21 July 2017, 13:25:02 UTC | restart the proof of cramershoup | 21 July 2017, 13:32:33 UTC |
| d831de8 | Benjamin Gregoire | 21 July 2017, 13:24:11 UTC | more lemma on distribution | 21 July 2017, 13:32:33 UTC |
| 7dccbf0 | Benjamin Gregoire | 21 July 2017, 13:23:51 UTC | Fix error in the definition of PKE (cstar was not initialised) | 21 July 2017, 13:32:33 UTC |
| 78c7d52 | Benjamin Gregoire | 21 July 2017, 13:21:38 UTC | add the ceil and floor functions | 21 July 2017, 13:32:33 UTC |
| ebadb1b | Benjamin Gregoire | 21 July 2017, 13:21:02 UTC | fix bug in bypr and put some condition in the good order. | 21 July 2017, 13:32:33 UTC |
| e425db8 | François Dupressoir | 19 July 2017, 21:52:54 UTC | BR93 example: refactor to illustrate instantiation More work is needed to clean definitions and final statement up. | 19 July 2017, 21:52:54 UTC |
| c552f14 | François Dupressoir | 11 July 2017, 14:55:24 UTC | Hash ElGamal (Generic): ported. | 11 July 2017, 14:55:24 UTC |
| 0fb20bc | François Dupressoir | 11 July 2017, 12:49:01 UTC | VonNeumann: ported. | 11 July 2017, 12:49:01 UTC |
| e4cdb04 | François Dupressoir | 11 July 2017, 12:38:21 UTC | BR93: use \in for sets. | 11 July 2017, 12:38:21 UTC |
| 183c9a5 | François Dupressoir | 11 July 2017, 12:26:05 UTC | FSet: add \in notation | 11 July 2017, 12:26:05 UTC |
| b2071e1 | François Dupressoir | 11 July 2017, 12:16:41 UTC | PRG: more nits | 11 July 2017, 12:16:41 UTC |
| 1558277 | François Dupressoir | 11 July 2017, 12:16:17 UTC | (Hashed) ElGamal: ported | 11 July 2017, 12:16:17 UTC |
| 204eb6f | François Dupressoir | 11 July 2017, 07:03:26 UTC | PRG: pWhile assignment notation | 11 July 2017, 07:03:26 UTC |
| d8d89a3 | François Dupressoir | 10 July 2017, 09:26:20 UTC | BR93: removing progress. | 10 July 2017, 09:26:20 UTC |
| 765d68c | François Dupressoir | 10 July 2017, 09:26:11 UTC | PRG: ported. | 10 July 2017, 09:26:11 UTC |
| ce8d888 | François Dupressoir | 10 July 2017, 08:01:07 UTC | BR93: cleanup, limiting smt, clarity. | 10 July 2017, 08:01:07 UTC |
| a73ed57 | François Dupressoir | 07 July 2017, 21:33:02 UTC | BR93: further cleanup and lib extensions | 07 July 2017, 21:33:02 UTC |
| 6390747 | François Dupressoir | 04 July 2017, 22:46:09 UTC | MEE-CBC: Ported? | 04 July 2017, 22:46:09 UTC |
| 5068ae6 | François Dupressoir | 04 July 2017, 21:55:50 UTC | BR93: Fixed after stdlib changes. | 04 July 2017, 21:55:50 UTC |
| 7af9061 | François Dupressoir | 04 July 2017, 20:46:22 UTC | Theory Word: clone MFinite rather than ad hoc redef | 04 July 2017, 20:46:26 UTC |
| e6cd83e | François Dupressoir | 04 July 2017, 19:22:03 UTC | BR93: use BitWord, some renaming AWord is deprecated and should not be used. | 04 July 2017, 19:22:11 UTC |
| a2ad181 | François Dupressoir | 04 July 2017, 09:33:49 UTC | BR93: ported | 04 July 2017, 09:34:05 UTC |
| dea2238 | Pierre-Yves Strub | 28 June 2017, 08:15:23 UTC | Docker doc box | 28 June 2017, 08:15:23 UTC |
| 0f658e6 | Pierre-Yves Strub | 15 June 2017, 11:18:48 UTC | Bug fix in cloning. When aliasing a theory, do alias the constructors path of the enclosed datatypes. | 15 June 2017, 11:18:48 UTC |
| d6e9a3c | Cécile BARITEL-RUET | 15 June 2017, 08:21:56 UTC | New tactic: `replace`. Extension to `transitivity` that allows to construct the intermediate program via pattern matching and back-references. | 15 June 2017, 08:21:56 UTC |
| b1b1a1e | Pierre-Yves Strub | 15 June 2017, 08:19:25 UTC | API: generic tree regexp matcher. | 15 June 2017, 08:19:25 UTC |
| 8c21183 | Pierre-Yves Strub | 15 June 2017, 08:05:54 UTC | Misc: add explicit entry point for EC | 15 June 2017, 08:05:54 UTC |
| 449d0f2 | Pierre-Yves Strub | 15 June 2017, 08:05:25 UTC | Internals: remove unimplemented `ByPattern case for [inline] | 15 June 2017, 08:05:25 UTC |
| d49a3f6 | Pierre-Yves Strub | 13 June 2017, 20:31:03 UTC | Travis | 13 June 2017, 20:31:03 UTC |
| 1953e05 | Pierre-Yves Strub | 02 June 2017, 08:17:00 UTC | Column/lineno pretty-printer for statements | 02 June 2017, 08:17:14 UTC |
| 908afa4 | Francois Dupressoir | 17 May 2017, 14:12:10 UTC | README.md: Fix opam prefix | 17 May 2017, 14:12:10 UTC |
| 7cb1468 | Pierre-Yves Strub | 26 April 2017, 17:17:47 UTC | README | 26 April 2017, 17:17:47 UTC |
| a8c2c61 | Pierre-Yves Strub | 07 April 2017, 12:08:01 UTC | List: all_count_in | 07 April 2017, 12:08:01 UTC |
| b4866ca | Pierre-Yves Strub | 27 March 2017, 12:30:31 UTC | Travis: reporting | 27 March 2017, 12:31:22 UTC |
| 1079832 | Benjamin Gregoire | 24 March 2017, 13:19:27 UTC | Use “is_lossless” and "predT" in rnd rules instead of their expansions | 24 March 2017, 13:19:27 UTC |
| 4950e67 | Benjamin Gregoire | 22 March 2017, 08:55:29 UTC | add the “selected” option to smt tactic the option prints the list of selected lemmas which are sent to smt. | 22 March 2017, 08:59:38 UTC |
| 4f24928 | Pierre-Yves Strub | 21 March 2017, 19:45:07 UTC | Merging NewLogic & Logic, removing old API | 21 March 2017, 19:45:23 UTC |
| 91d7e7d | Pierre-Yves Strub | 20 March 2017, 19:14:22 UTC | Fix all admits in Tuple | 20 March 2017, 19:14:22 UTC |
| 17ab666 | Benjamin Gregoire | 20 March 2017, 15:33:59 UTC | Switching EasyCrypt && stdlib to new distributions library | 20 March 2017, 15:33:59 UTC |
| ebd097f | Pierre-Yves Strub | 20 March 2017, 09:19:34 UTC | Fixing all admits in List | 20 March 2017, 09:19:34 UTC |
| 061186a | Pierre-Yves Strub | 19 March 2017, 21:59:49 UTC | Restore PrimeField.ec | 19 March 2017, 21:59:49 UTC |
| 221aca5 | Pierre-Yves Strub | 19 March 2017, 21:04:37 UTC | Remove unused theories | 19 March 2017, 21:04:37 UTC |
| 32a4616 | Pierre-Yves Strub | 19 March 2017, 18:14:19 UTC | increase default timeout | 19 March 2017, 18:14:19 UTC |
| 451b29d | Pierre-Yves Strub | 19 March 2017, 18:05:54 UTC | Travis: check examples | 19 March 2017, 18:05:54 UTC |
| acdc38f | Pierre-Yves Strub | 19 March 2017, 18:03:08 UTC | Move all examples in examples/old/ Have to be moved back when ported. | 19 March 2017, 18:03:08 UTC |
| abd8e9a | Pierre-Yves Strub | 19 March 2017, 13:50:37 UTC | Adapt stdlib to new Int.ec | 19 March 2017, 13:50:37 UTC |
| ec2fa26 | Pierre-Yves Strub | 19 March 2017, 13:37:00 UTC | Splitting and fixing Int.ec | 19 March 2017, 13:37:14 UTC |
| d09c1a7 | Pierre-Yves Strub | 19 March 2017, 10:53:21 UTC | Killing admits in StdBigop. | 19 March 2017, 10:53:21 UTC |
| 67e0bba | Pierre-Yves Strub | 19 March 2017, 10:53:13 UTC | [bigop]: big_flatten | 19 March 2017, 10:53:13 UTC |
| 4b2cc9e | Pierre-Yves Strub | 19 March 2017, 10:53:01 UTC | [list]: basic facts on `count` (count_pred0_eq, count_pred_eq) | 19 March 2017, 10:53:01 UTC |
| 91de244 | Benjamin Gregoire | 18 March 2017, 17:14:16 UTC | add surjective predicate | 19 March 2017, 10:22:14 UTC |
| aa1442d | Pierre-Yves Strub | 19 March 2017, 10:21:37 UTC | [bigop]: perm_eq_big_map | 19 March 2017, 10:21:37 UTC |
| 5e3445f | Pierre-Yves Strub | 19 March 2017, 10:14:37 UTC | [list]: perm_eq_rev | 19 March 2017, 10:14:37 UTC |
| 54d6905 | Benjamin Gregoire | 19 March 2017, 07:32:27 UTC | add lemma on big and < | 19 March 2017, 10:09:31 UTC |
| 3a7368f | Pierre-Yves Strub | 18 March 2017, 11:30:18 UTC | Makefile: fix deps-a | 18 March 2017, 11:30:18 UTC |
| 5cef9de | Pierre-Yves Strub | 18 March 2017, 11:25:57 UTC | substitution TARGETS in travis file | 18 March 2017, 11:25:57 UTC |
| b4427d7 | Pierre-Yves Strub | 18 March 2017, 11:10:16 UTC | Nits in travis | 18 March 2017, 11:13:42 UTC |
| 5b99fff | Benjamin Gregoire | 18 March 2017, 11:08:20 UTC | Fix ROM example | 18 March 2017, 11:08:35 UTC |
| 98db241 | Pierre-Yves Strub | 18 March 2017, 10:01:59 UTC | separate stdlib check from ec compilation | 18 March 2017, 10:01:59 UTC |
| 39edcd2 | Pierre-Yves Strub | 18 March 2017, 09:53:11 UTC | Fix compilation of IntDiv | 18 March 2017, 09:53:11 UTC |
| 546553d | Pierre-Yves Strub | 18 March 2017, 07:48:47 UTC | Travis: check stdlib | 18 March 2017, 07:48:47 UTC |
| 551232c | Pierre-Yves Strub | 17 March 2017, 13:09:42 UTC | partition_big: generalize types | 17 March 2017, 13:09:52 UTC |
| 2a46a2e | Benjamin Gregoire | 17 March 2017, 11:38:15 UTC | Fix printing of random assignment | 17 March 2017, 12:50:16 UTC |
| 0b0bfec | Pierre-Yves Strub | 16 March 2017, 08:58:44 UTC | [list]: zip/unzip + facts | 16 March 2017, 08:58:44 UTC |
| 0f68ed7 | Pierre-Yves Strub | 15 March 2017, 13:41:10 UTC | Travis: test all branches marked for future integration | 15 March 2017, 13:41:10 UTC |
| 807b27e | Pierre-Yves Strub | 05 March 2017, 23:30:36 UTC | README | 05 March 2017, 23:30:36 UTC |
| f85539c | Pierre-Yves Strub | 04 March 2017, 22:11:04 UTC | docker (nits) | 04 March 2017, 22:11:04 UTC |
| 572f035 | Pierre-Yves Strub | 04 March 2017, 21:08:33 UTC | nits in docker (aprhl) | 04 March 2017, 21:08:33 UTC |
| ccea93c | Pierre-Yves Strub | 04 March 2017, 20:38:03 UTC | nits in docker | 04 March 2017, 20:38:12 UTC |
| fd2fc2b | Pierre-Yves Strub | 04 March 2017, 09:35:08 UTC | Add support for system level conf. file Format: ini file. Sections: [general]. Options: - why3conf (string) : Why3 configuration file - provers (string list) : -P option (list of used provers) - idirs (string list) : -I option - rdirs (string list) : -R option - no-evict (string list) : -no-evict option INI file location: EasyCrypt lib. directory /etc/easycrypt.ini | 04 March 2017, 09:35:15 UTC |
| 4afed9d | Pierre-Yves Strub | 04 March 2017, 08:37:24 UTC | remove code dedicated to local toolchain | 04 March 2017, 08:38:49 UTC |
| d633c86 | Pierre-Yves Strub | 04 March 2017, 08:27:26 UTC | update files headers (libraries) (copyright) | 04 March 2017, 08:27:26 UTC |
| cd4a4d0 | Pierre-Yves Strub | 04 March 2017, 08:26:41 UTC | update files headers (copyright) | 04 March 2017, 08:26:41 UTC |
| 42ecbc7 | Pierre-Yves Strub | 04 March 2017, 08:26:04 UTC | Fix compilation issues | 04 March 2017, 08:26:04 UTC |
| 7519681 | Pierre-Yves Strub | 04 March 2017, 08:23:12 UTC | update copyright meta-data (bis) | 04 March 2017, 08:23:12 UTC |
| 532fd5d | Pierre-Yves Strub | 04 March 2017, 08:19:21 UTC | update copyright meta-data | 04 March 2017, 08:19:21 UTC |
| 249f7c1 | Pierre-Yves Strub | 02 March 2017, 09:55:54 UTC | README (opam pin) | 02 March 2017, 09:55:54 UTC |
| 2ebb404 | Pierre-Yves Strub | 02 March 2017, 09:55:36 UTC | [docker]: generic test box | 02 March 2017, 09:55:36 UTC |
| a16c59a | Pierre-Yves Strub | 01 March 2017, 22:19:33 UTC | [README]: installing ec-branches via opam | 01 March 2017, 22:19:33 UTC |
| 8b2bf22 | Pierre-Yves Strub | 01 March 2017, 22:07:07 UTC | Nits on docker boxes | 01 March 2017, 22:07:07 UTC |
| 624a583 | Pierre-Yves Strub | 01 March 2017, 14:34:59 UTC | docker box for CI (tests) | 01 March 2017, 14:34:59 UTC |
| dc91673 | Pierre-Yves Strub | 01 March 2017, 12:25:26 UTC | testting -> testing | 01 March 2017, 12:25:26 UTC |
| a7c115c | Pierre-Yves Strub | 01 March 2017, 12:21:50 UTC | [make install] installs the runtest binary | 01 March 2017, 12:21:50 UTC |
| bd3b7b0 | Pierre-Yves Strub | 01 March 2017, 12:21:34 UTC | Use the correct env. when printing synced prhl goals | 01 March 2017, 12:21:34 UTC |
| da54edb | Pierre-Yves Strub | 01 March 2017, 11:04:22 UTC | [pprint]: when checking that 2 programs are in sync, use alpha-eq without path norm'ion | 01 March 2017, 11:04:22 UTC |
| d92f237 | Pierre-Yves Strub | 01 March 2017, 10:59:06 UTC | API: access to alpha-conversion without path norm'ion | 01 March 2017, 10:59:06 UTC |
| 3e41975 | Pierre-Yves Strub | 01 March 2017, 10:03:32 UTC | Do not try to install non-existent PG files | 01 March 2017, 10:03:32 UTC |
| df7ff31 | Pierre-Yves Strub | 01 March 2017, 09:45:31 UTC | Fix english | 01 March 2017, 09:45:31 UTC |
| 2950852 | Pierre-Yves Strub | 01 March 2017, 09:44:45 UTC | [pprint]: in prhl, when program as sync'ed, only display one | 01 March 2017, 09:44:45 UTC |
| 8f58725 | Pierre-Yves Strub | 27 February 2017, 13:18:47 UTC | README (travis status) | 27 February 2017, 13:18:47 UTC |
| 372fed8 | Pierre-Yves Strub | 27 February 2017, 13:14:53 UTC | Docker boxes | 27 February 2017, 13:14:53 UTC |
