f47fb53 | Cécile BARITEL-RUET | 26 November 2019, 07:51:24 UTC | better with the files | 26 November 2019, 07:51:24 UTC |
dc9e664 | Cécile BARITEL-RUET | 26 November 2019, 07:50:49 UTC | attempt to chacha-poly | 26 November 2019, 07:50:49 UTC |
8134d1a | Cécile BARITEL-RUET | 16 September 2019, 15:56:04 UTC | fix | 16 September 2019, 15:56:04 UTC |
4af3bf7 | Cécile BARITEL-RUET | 16 September 2019, 15:11:06 UTC | Merge branch '1.0' into deploy-fmatch | 16 September 2019, 15:11:06 UTC |
67392e1 | Cécile BARITEL-RUET | 16 September 2019, 12:54:52 UTC | RndProd : random oracle of a dprod | 16 September 2019, 12:56:20 UTC |
a8e2f10 | Pierre-Yves Strub | 15 September 2019, 12:05:31 UTC | Fix defered start of provers | 15 September 2019, 16:59:56 UTC |
7641f4a | Benjamin Gregoire | 13 September 2019, 14:21:19 UTC | merge RndO and PROM | 13 September 2019, 14:21:19 UTC |
2e91082 | Cécile BARITEL-RUET | 13 September 2019, 12:56:12 UTC | old modifications | 13 September 2019, 12:56:12 UTC |
3d66517 | Benjamin Gregoire | 13 September 2019, 11:17:04 UTC | import DHIES | 13 September 2019, 11:17:04 UTC |
2c5203d | Pierre-Yves Strub | 13 September 2019, 11:01:05 UTC | more on lists (assoc, onth) + some facts on fmap/assoc | 13 September 2019, 11:01:20 UTC |
13b7bdd | Benjamin Gregoire | 13 September 2019, 09:49:36 UTC | add PKSMK | 13 September 2019, 09:49:36 UTC |
3bbc09b | Benjamin Gregoire | 13 September 2019, 09:39:56 UTC | add AEAD | 13 September 2019, 09:39:56 UTC |
746d64c | Pierre-Yves Strub | 13 September 2019, 08:30:58 UTC | Revert "remove duplicate lemma get_none -> domNE" This reverts commit 60d29c1f11f6c79824022608f9f83503d983ce61. | 13 September 2019, 08:30:58 UTC |
0344765 | Pierre-Yves Strub | 13 September 2019, 08:20:36 UTC | djoin and al | 13 September 2019, 08:20:36 UTC |
60d29c1 | Benjamin Gregoire | 13 September 2019, 06:39:19 UTC | remove duplicate lemma get_none -> domNE | 13 September 2019, 06:39:19 UTC |
0e717db | Pierre-Yves Strub | 12 September 2019, 21:17:28 UTC | pre/post selector Syntax if #rg?name where `name` is either `pre` or `post` and `rg` is a list of filters. | 12 September 2019, 21:18:52 UTC |
806fa6b | Pierre-Yves Strub | 12 September 2019, 20:57:15 UTC | Fix compilation | 12 September 2019, 20:57:15 UTC |
2dd053c | Benjamin Gregoire | 12 September 2019, 19:05:48 UTC | add assumption | 12 September 2019, 20:35:16 UTC |
7fb964c | Benjamin Gregoire | 12 September 2019, 19:01:35 UTC | add generalized oracle Diffie-Hellman assumption | 12 September 2019, 20:35:16 UTC |
350728b | Benjamin Gregoire | 12 September 2019, 18:05:03 UTC | add hash colision resistant assumption | 12 September 2019, 20:35:16 UTC |
0f3ebba | Pierre-Yves Strub | 12 September 2019, 19:10:51 UTC | dlet-sampling : distr are now parameters | 12 September 2019, 19:10:51 UTC |
65e3d88 | Pierre-Yves Strub | 12 September 2019, 14:21:46 UTC | eqv between dlet-sampling and seq-sampling | 12 September 2019, 14:21:46 UTC |
6ec8512 | Benjamin Gregoire | 12 September 2019, 12:26:49 UTC | fix trivial error | 12 September 2019, 12:26:49 UTC |
786cb63 | Benjamin Gregoire | 12 September 2019, 12:18:07 UTC | Add generic Lazy/Eager for random oracle | 12 September 2019, 12:18:29 UTC |
e5efb23 | Pierre-Yves Strub | 06 September 2019, 13:48:52 UTC | Refactor and kill all admits related to distributions and infinite sums. | 06 September 2019, 13:48:52 UTC |
60b76e8 | Benjamin Gregoire | 05 September 2019, 09:05:32 UTC | Try to remove exponential behavior | 05 September 2019, 09:05:32 UTC |
2e3a618 | Benjamin Gregoire | 04 September 2019, 13:31:51 UTC | use abstract theory | 04 September 2019, 13:31:51 UTC |
84dc271 | Benjamin Gregoire | 04 September 2019, 07:11:42 UTC | remove unused variable | 04 September 2019, 07:11:42 UTC |
132aa51 | Benjamin Gregoire | 03 September 2019, 14:35:01 UTC | Add few lemmas | 03 September 2019, 14:35:01 UTC |
0a6c7f8 | Benjamin Gregoire | 03 September 2019, 08:54:33 UTC | Proving probability equal to 1/2 using prhl | 03 September 2019, 08:55:55 UTC |
a4fb49d | Pierre-Yves Strub | 04 August 2019, 19:07:17 UTC | fix Why3 literals comparisons [fix #17394] | 04 August 2019, 19:07:17 UTC |
af281fd | Pierre-Yves Strub | 02 August 2019, 20:16:22 UTC | Do eta-expansion for fix-match branches [fix #17385] | 02 August 2019, 20:16:22 UTC |
43ac3f3 | Benjamin Gregoire | 22 July 2019, 16:54:24 UTC | Fix bug in subst of type definition (parameters were not substituted) | 22 July 2019, 16:54:24 UTC |
a9666b1 | Pierre-Yves Strub | 06 July 2019, 22:07:08 UTC | user error message for FXE_CtorInvalidArity [fix #17387] | 06 July 2019, 22:07:21 UTC |
af25c22 | Benjamin Gregoire | 19 June 2019, 13:28:03 UTC | Bug fixing in phl ([closes #17380]) | 19 June 2019, 13:28:03 UTC |
fc8d388 | Pierre-Yves Strub | 11 June 2019, 09:59:50 UTC | Move to Why3 1.x | 11 June 2019, 09:59:50 UTC |
43e5a65 | Cécile BARITEL-RUET | 04 June 2019, 12:45:24 UTC | some cleaning | 04 June 2019, 12:45:24 UTC |
fbd3468 | Cécile BARITEL-RUET | 04 June 2019, 12:33:29 UTC | simple fix for Zand when empty | 04 June 2019, 12:33:29 UTC |
9dbfd56 | Cécile BARITEL-RUET | 04 June 2019, 12:29:49 UTC | some fix | 04 June 2019, 12:29:49 UTC |
0e9b41e | Cécile BARITEL-RUET | 04 June 2019, 11:44:48 UTC | fmatching and genregexp are mutually recursive | 04 June 2019, 11:44:48 UTC |
679f333 | Pierre-Yves Strub | 17 May 2019, 05:46:17 UTC | run-test: add a -timing option | 17 May 2019, 05:46:17 UTC |
a79235c | Pierre-Yves Strub | 17 May 2019, 05:34:41 UTC | add an option [-tstats FILE] for recording timing statistics | 17 May 2019, 05:34:41 UTC |
e522b67 | Pierre-Yves Strub | 01 May 2019, 07:37:32 UTC | runtest: python2 -> python3 | 01 May 2019, 07:37:32 UTC |
f293e76 | François Dupressoir | 16 April 2019, 15:21:17 UTC | Towards fixing XDG-based config | 16 April 2019, 16:18:33 UTC |
bfa4f3e | Cécile BARITEL-RUET | 08 April 2019, 10:36:40 UTC | . | 08 April 2019, 10:36:40 UTC |
ce2ceb7 | Cécile BARITEL-RUET | 02 April 2019, 07:32:37 UTC | . | 02 April 2019, 07:32:37 UTC |
27c1df3 | Pierre-Yves Strub | 28 March 2019, 05:41:39 UTC | Allow : t1 || t2 || ... || tn | 28 March 2019, 05:41:39 UTC |
9ae843f | Cécile BARITEL-RUET | 27 March 2019, 16:48:30 UTC | Second try. Still does not work. | 27 March 2019, 16:48:30 UTC |
82c7541 | Cécile BARITEL-RUET | 27 March 2019, 15:34:44 UTC | First try. Does not work. | 27 March 2019, 15:34:44 UTC |
41219ef | Pierre-Yves Strub | 26 March 2019, 13:42:33 UTC | add reduction of Int div/mod by reduction of edivz + bind symbol to Why3 | 26 March 2019, 13:42:33 UTC |
a041441 | Pierre-Yves Strub | 26 March 2019, 13:32:42 UTC | Add congruence rule for projections | 26 March 2019, 13:32:42 UTC |
5e9f955 | Pierre-Yves Strub | 26 March 2019, 10:46:03 UTC | Extend matching (projections) | 26 March 2019, 10:46:03 UTC |
8a0c097 | Pierre-Yves Strub | 26 March 2019, 09:59:05 UTC | Bind auto-conseq in eqobsin | 26 March 2019, 09:59:05 UTC |
b481f98 | Pierre-Yves Strub | 25 March 2019, 12:03:45 UTC | "call L" automatically applies "L" to "_" when needed. | 25 March 2019, 12:03:45 UTC |
1fb57b6 | Pierre-Yves Strub | 25 March 2019, 08:07:17 UTC | fix reduction of fixpoints with extra arguments | 25 March 2019, 08:07:17 UTC |
0a33156 | Pierre-Yves Strub | 24 March 2019, 09:08:50 UTC | try to convert closed pattern before failing... | 24 March 2019, 09:08:50 UTC |
16d3bf4 | Pierre-Yves Strub | 23 March 2019, 18:47:22 UTC | | 23 March 2019, 18:47:22 UTC |
3515767 | Pierre-Yves Strub | 23 March 2019, 18:38:20 UTC | | 23 March 2019, 18:38:20 UTC |
6c91e46 | Pierre-Yves Strub | 23 March 2019, 18:29:13 UTC | | 23 March 2019, 18:29:13 UTC |
091db62 | Cécile BARITEL-RUET | 22 March 2019, 16:44:17 UTC | fix crypto/rom/Lazy.eca script (after fixing fun_ext) | 22 March 2019, 16:44:17 UTC |
19680a9 | Cécile BARITEL-RUET | 22 March 2019, 16:34:18 UTC | fix eta | 22 March 2019, 16:34:18 UTC |
972a0fa | Cécile BARITEL-RUET | 22 March 2019, 16:02:09 UTC | fix eta-reduction/eta-extension | 22 March 2019, 16:02:09 UTC |
5cb65da | Cécile BARITEL-RUET | 22 March 2019, 15:22:15 UTC | fix computing of free variables in patterns | 22 March 2019, 15:22:15 UTC |
da94e33 | Cécile BARITEL-RUET | 22 March 2019, 14:13:43 UTC | correct version of fun_ext to match the one in 1.0 | 22 March 2019, 14:13:43 UTC |
8ee2bc5 | Cécile BARITEL-RUET | 22 March 2019, 14:01:16 UTC | . | 22 March 2019, 14:01:16 UTC |
70e1b67 | Cécile BARITEL-RUET | 19 March 2019, 14:42:29 UTC | 4 bugs left | 19 March 2019, 14:42:29 UTC |
dd4d51a | Cécile BARITEL-RUET | 19 March 2019, 14:02:52 UTC | managing restrictions about mhr | 19 March 2019, 14:02:52 UTC |
86fce7d | Cécile BARITEL-RUET | 19 March 2019, 13:37:41 UTC | test | 19 March 2019, 13:37:41 UTC |
2babf50 | Cécile BARITEL-RUET | 19 March 2019, 13:27:25 UTC | fix last commit | 19 March 2019, 13:27:25 UTC |
5d1bb0f | Cécile BARITEL-RUET | 19 March 2019, 13:15:51 UTC | change reduction continuations | 19 March 2019, 13:15:51 UTC |
ef5eaa2 | Cécile BARITEL-RUET | 19 March 2019, 11:40:34 UTC | allow use of mhr | 19 March 2019, 11:40:34 UTC |
b80c242 | Cécile BARITEL-RUET | 19 March 2019, 10:18:17 UTC | fix infinite loop | 19 March 2019, 10:18:17 UTC |
9f349d7 | Cécile BARITEL-RUET | 19 March 2019, 09:29:59 UTC | fix matching same meta | 19 March 2019, 09:29:59 UTC |
42bee10 | Cécile BARITEL-RUET | 18 March 2019, 14:57:22 UTC | fix reduction | 18 March 2019, 14:57:22 UTC |
d5ccd83 | Cécile BARITEL-RUET | 18 March 2019, 12:21:32 UTC | fix reduction | 18 March 2019, 12:21:32 UTC |
b2b6502 | Cécile BARITEL-RUET | 18 March 2019, 10:14:38 UTC | fix reduction | 18 March 2019, 10:14:38 UTC |
530ccdd | Cécile BARITEL-RUET | 18 March 2019, 09:33:39 UTC | fix reduction of (=) | 18 March 2019, 09:33:39 UTC |
e8d6aef | Cécile BARITEL-RUET | 18 March 2019, 09:21:49 UTC | fix reductions | 18 March 2019, 09:21:49 UTC |
6019ae3 | Cécile BARITEL-RUET | 14 March 2019, 16:51:48 UTC | fix infinite loop | 14 March 2019, 16:51:48 UTC |
9031f24 | Cécile BARITEL-RUET | 14 March 2019, 16:11:26 UTC | no reduction in args of logical application | 14 March 2019, 16:11:26 UTC |
36b321b | Cécile BARITEL-RUET | 14 March 2019, 15:10:11 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 14 March 2019, 15:10:11 UTC |
b583880 | Cécile BARITEL-RUET | 14 March 2019, 15:09:59 UTC | modify verbose | 14 March 2019, 15:09:59 UTC |
17d07ee | Pierre-Yves Strub | 14 March 2019, 15:03:19 UTC | | 14 March 2019, 15:03:19 UTC |
89bf6be | Cécile BARITEL-RUET | 14 March 2019, 10:35:10 UTC | add verbose to ecPReduction | 14 March 2019, 10:35:10 UTC |
c2b2381 | Cécile BARITEL-RUET | 13 March 2019, 10:01:01 UTC | add EcFMatching.search_eng_head_no_delta | 13 March 2019, 10:01:01 UTC |
67f51b9 | Cécile BARITEL-RUET | 11 March 2019, 16:30:29 UTC | hide ecFmatching types | 11 March 2019, 16:30:29 UTC |
4f92c1b | Cécile BARITEL-RUET | 11 March 2019, 15:33:21 UTC | fix bug | 11 March 2019, 15:33:21 UTC |
7821071 | Cécile BARITEL-RUET | 11 March 2019, 12:21:15 UTC | fix stack overflow | 11 March 2019, 12:21:15 UTC |
a221d83 | Cécile BARITEL-RUET | 07 March 2019, 16:04:49 UTC | fix order of reduce tries | 07 March 2019, 16:04:49 UTC |
188f91f | Cécile BARITEL-RUET | 07 March 2019, 12:47:49 UTC | bug fix | 07 March 2019, 12:47:49 UTC |
b289db5 | Cécile BARITEL-RUET | 07 March 2019, 12:18:57 UTC | fix bugs | 07 March 2019, 12:18:57 UTC |
8d9152d | Cécile BARITEL-RUET | 07 March 2019, 10:23:15 UTC | bug fixes | 07 March 2019, 10:23:15 UTC |
012a2b1 | Cécile BARITEL-RUET | 07 March 2019, 10:00:37 UTC | fix bug in p_subst when pat_local | 07 March 2019, 10:00:37 UTC |
26e0600 | Cécile BARITEL-RUET | 07 March 2019, 09:47:39 UTC | menv_is_full now checks if unienv is closed | 07 March 2019, 09:47:39 UTC |
d851a97 | Cécile BARITEL-RUET | 06 March 2019, 17:12:58 UTC | forgot to add ecPReduction | 06 March 2019, 17:12:58 UTC |
979e9bc | Cécile BARITEL-RUET | 06 March 2019, 17:08:33 UTC | . | 06 March 2019, 17:08:33 UTC |
d2845bc | Cécile BARITEL-RUET | 06 March 2019, 14:19:31 UTC | fix higher order | 06 March 2019, 14:19:31 UTC |
9e3d6df | Cécile BARITEL-RUET | 06 March 2019, 13:45:15 UTC | restrict higher order case when higher order unification is decidable. | 06 March 2019, 13:45:15 UTC |
4aaf661 | Cécile BARITEL-RUET | 06 March 2019, 10:12:22 UTC | fix eta-reduction | 06 March 2019, 10:12:22 UTC |
04e9c66 | Cécile BARITEL-RUET | 05 March 2019, 17:17:26 UTC | fix simplification of Int(+) and Real.(+) | 05 March 2019, 17:17:26 UTC |