2452b4a | Cécile BARITEL-RUET | 05 March 2019, 15:20:35 UTC | fix higher order | 05 March 2019, 15:20:35 UTC |
08f34f3 | Cécile BARITEL-RUET | 05 March 2019, 12:27:08 UTC | fix minor bug | 05 March 2019, 12:27:08 UTC |
03c538f | Cécile BARITEL-RUET | 05 March 2019, 12:19:06 UTC | fix minor bug | 05 March 2019, 12:19:06 UTC |
1447687 | Cécile BARITEL-RUET | 05 March 2019, 12:09:10 UTC | fix bug | 05 March 2019, 12:09:10 UTC |
4761a76 | Cécile BARITEL-RUET | 01 March 2019, 14:13:03 UTC | How many files does (matching -> unification) break ? | 01 March 2019, 14:13:03 UTC |
12f3528 | Cécile BARITEL-RUET | 28 February 2019, 10:31:01 UTC | add substitution to the formula when processing matching. | 28 February 2019, 10:31:01 UTC |
ef093d0 | Cécile BARITEL-RUET | 25 February 2019, 16:39:41 UTC | fix infinite loop in crypto/ROM.ec | 25 February 2019, 16:39:41 UTC |
a8f3c44 | Cécile BARITEL-RUET | 25 February 2019, 16:27:19 UTC | fix an infinite loop. Now reductions of logical operations output if the simplifications have been made. | 25 February 2019, 16:27:19 UTC |
d5bf3fc | Cécile BARITEL-RUET | 25 February 2019, 15:15:42 UTC | fix Core.ec script. | 25 February 2019, 15:15:42 UTC |
dcdb504 | Cécile BARITEL-RUET | 25 February 2019, 14:27:24 UTC | quit checking if reduction's output is same as input. | 25 February 2019, 14:27:24 UTC |
a51e982 | Cécile BARITEL-RUET | 25 February 2019, 13:50:23 UTC | . | 25 February 2019, 13:50:23 UTC |
4f82c26 | Cécile BARITEL-RUET | 25 February 2019, 13:47:35 UTC | test | 25 February 2019, 13:47:35 UTC |
acfd6d1 | Cécile BARITEL-RUET | 25 February 2019, 10:32:46 UTC | fix 1 stack overflow | 25 February 2019, 10:32:46 UTC |
5339596 | Cécile BARITEL-RUET | 20 February 2019, 15:13:48 UTC | fix minor bug | 20 February 2019, 15:13:48 UTC |
32e5b18 | Cécile BARITEL-RUET | 20 February 2019, 14:44:11 UTC | fix InvalidProofTerm bug | 20 February 2019, 14:44:11 UTC |
ab18e4d | Pierre-Yves Strub | 20 February 2019, 13:29:34 UTC | | 20 February 2019, 13:30:02 UTC |
f234005 | Cécile BARITEL-RUET | 20 February 2019, 12:58:07 UTC | fix simplifications of Int.(+) | 20 February 2019, 12:58:07 UTC |
e920d43 | Cécile BARITEL-RUET | 20 February 2019, 12:19:00 UTC | added eta-expansion (if possible according to type checking) | 20 February 2019, 12:19:00 UTC |
9929200 | Cécile BARITEL-RUET | 20 February 2019, 11:18:42 UTC | in p_int_lt_simpl, p_int_le was used... | 20 February 2019, 11:18:42 UTC |
1944a29 | Cécile BARITEL-RUET | 19 February 2019, 16:42:26 UTC | in the head reduction : added a case when both are applications, and their operator are "formula", then if they are equal, no reduction will make the matching work | 19 February 2019, 16:42:26 UTC |
5d44156 | Cécile BARITEL-RUET | 19 February 2019, 15:41:38 UTC | fix bug when reducing in a non-higher-order case keeps track of the non-higher-orderness | 19 February 2019, 15:41:38 UTC |
09ede79 | Cécile BARITEL-RUET | 19 February 2019, 13:31:33 UTC | . | 19 February 2019, 13:31:33 UTC |
2e4a2fe | Cécile BARITEL-RUET | 19 February 2019, 12:41:37 UTC | . | 19 February 2019, 12:41:37 UTC |
1d986d0 | Cécile BARITEL-RUET | 19 February 2019, 12:33:39 UTC | . | 19 February 2019, 12:33:39 UTC |
62e6374 | Cécile BARITEL-RUET | 19 February 2019, 10:45:54 UTC | count bugs | 19 February 2019, 10:45:54 UTC |
45e1db8 | Cécile BARITEL-RUET | 19 February 2019, 09:41:07 UTC | fix 1 bug (or more ?) | 19 February 2019, 09:41:07 UTC |
8bda7a4 | Cécile BARITEL-RUET | 18 February 2019, 18:00:00 UTC | fix 1 bug | 18 February 2019, 18:00:00 UTC |
eb7460d | Pierre-Yves Strub | 16 February 2019, 05:39:03 UTC | | 16 February 2019, 05:39:12 UTC |
66c21ca | Cécile BARITEL-RUET | 15 February 2019, 15:00:16 UTC | . | 15 February 2019, 15:00:16 UTC |
b082aa4 | Pierre-Yves Strub | 15 February 2019, 06:46:01 UTC | | 15 February 2019, 06:46:01 UTC |
6532318 | Cécile BARITEL-RUET | 14 February 2019, 14:37:32 UTC | . | 14 February 2019, 14:37:32 UTC |
c4c4748 | Cécile BARITEL-RUET | 14 February 2019, 13:33:20 UTC | adding an option to print debug verbose in "rewrite <<*>> ..." and "move <<*>> => /..." | 14 February 2019, 13:33:20 UTC |
f573272 | Cécile BARITEL-RUET | 14 February 2019, 10:36:50 UTC | bug fix | 14 February 2019, 10:36:50 UTC |
67bf54b | Cécile BARITEL-RUET | 13 February 2019, 15:15:45 UTC | remove some infinite loops | 13 February 2019, 15:15:45 UTC |
e3f44bb | Cécile BARITEL-RUET | 13 February 2019, 14:32:43 UTC | . | 13 February 2019, 14:32:43 UTC |
4bf8561 | Pierre-Yves Strub | 13 February 2019, 13:50:41 UTC | removing dead code | 13 February 2019, 13:50:41 UTC |
00cf41e | Cécile BARITEL-RUET | 12 February 2019, 17:35:43 UTC | "function [p1;p2;p3] -> ... | _ -> assert false" replaced by as_seq3 | 12 February 2019, 17:35:43 UTC |
3fac364 | Cécile BARITEL-RUET | 12 February 2019, 16:43:04 UTC | cleaning + debugging | 12 February 2019, 16:43:04 UTC |
188aec2 | Cécile BARITEL-RUET | 12 February 2019, 12:02:16 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 12 February 2019, 12:02:16 UTC |
91d3b23 | Cécile BARITEL-RUET | 12 February 2019, 12:01:49 UTC | remove unused Zbinds | 12 February 2019, 12:01:49 UTC |
0b42571 | Pierre-Yves Strub | 12 February 2019, 11:56:37 UTC | | 12 February 2019, 11:56:37 UTC |
2644a06 | Cécile BARITEL-RUET | 12 February 2019, 10:46:00 UTC | clean matching rules | 12 February 2019, 10:46:00 UTC |
b9647ea | Cécile BARITEL-RUET | 08 February 2019, 13:04:18 UTC | lazy reduce instead of the eager one.. | 08 February 2019, 13:04:18 UTC |
b0c8dc3 | Pierre-Yves Strub | 06 February 2019, 17:30:31 UTC | | 06 February 2019, 17:30:31 UTC |
f37c69b | Pierre-Yves Strub | 06 February 2019, 17:09:40 UTC | | 06 February 2019, 17:09:40 UTC |
38aefa6 | Pierre-Yves Strub | 06 February 2019, 17:05:35 UTC | | 06 February 2019, 17:05:35 UTC |
5abfae3 | Pierre-Yves Strub | 06 February 2019, 16:56:57 UTC | | 06 February 2019, 16:56:57 UTC |
6cf5a33 | Pierre-Yves Strub | 06 February 2019, 16:20:12 UTC | | 06 February 2019, 16:20:12 UTC |
588dd7c | Pierre-Yves Strub | 06 February 2019, 08:12:52 UTC | fixing patterns for mpath/xpath | 06 February 2019, 08:12:52 UTC |
2078c00 | Pierre-Yves Strub | 04 February 2019, 20:57:24 UTC | | 04 February 2019, 20:57:24 UTC |
1cb1b75 | Cécile BARITEL-RUET | 04 February 2019, 14:05:06 UTC | parser conflit | 04 February 2019, 14:05:06 UTC |
69f500b | Pierre-Yves Strub | 03 February 2019, 08:33:21 UTC | rework patterns parser | 03 February 2019, 08:33:21 UTC |
05cea17 | Pierre-Yves Strub | 03 February 2019, 07:17:03 UTC | add entry point for pattern processing (test) | 03 February 2019, 07:17:03 UTC |
9067ffe | Pierre-Yves Strub | 03 February 2019, 07:12:37 UTC | move test file | 03 February 2019, 07:12:37 UTC |
95337e3 | Cécile BARITEL-RUET | 01 February 2019, 14:44:18 UTC | modify parser test + make an easycrypt file | 01 February 2019, 14:44:18 UTC |
5a64411 | Cécile BARITEL-RUET | 01 February 2019, 14:03:03 UTC | fix | 01 February 2019, 14:03:03 UTC |
d8fe2c8 | Cécile BARITEL-RUET | 01 February 2019, 13:59:41 UTC | simple fix on parser examples | 01 February 2019, 13:59:41 UTC |
4c9be47 | Cécile BARITEL-RUET | 01 February 2019, 13:42:50 UTC | a few examples of patterns | 01 February 2019, 13:42:50 UTC |
9cb4583 | Pierre-Yves Strub | 31 January 2019, 20:43:24 UTC | fixing rr & sr conflicts | 31 January 2019, 20:43:24 UTC |
a097dd7 | Cécile BARITEL-RUET | 31 January 2019, 16:09:18 UTC | merge stmt and instr | 31 January 2019, 16:09:18 UTC |
951e377 | Cécile BARITEL-RUET | 31 January 2019, 13:35:00 UTC | shift/reduce problems | 31 January 2019, 13:35:00 UTC |
4387903 | Pierre-Yves Strub | 28 January 2019, 13:48:44 UTC | Fix pretty printing of records projectors (when applied) | 28 January 2019, 13:48:44 UTC |
9c1fdfb | Pierre-Yves Strub | 28 January 2019, 13:40:40 UTC | Reduction fix: reduces record projections when applied. | 28 January 2019, 13:40:40 UTC |
a893051 | Benjamin Gregoire | 17 January 2019, 17:22:08 UTC | add missing quantification over memory in async while | 17 January 2019, 17:22:08 UTC |
b79b1fb | Cécile BARITEL-RUET | 20 December 2018, 15:00:23 UTC | fix bug where in Fapp (#x, args), #x was given the type of the application result, not the type of #x. | 20 December 2018, 15:00:23 UTC |
a8b8fa9 | Cécile BARITEL-RUET | 20 December 2018, 14:25:57 UTC | Merge branch '1.0' into deploy-fmatch | 20 December 2018, 14:25:57 UTC |
337a8ab | Cécile BARITEL-RUET | 20 December 2018, 14:25:05 UTC | fix a smt call | 20 December 2018, 14:25:05 UTC |
f6558b4 | Cécile BARITEL-RUET | 20 December 2018, 14:23:54 UTC | fix bug when the environment was restored in some cases | 20 December 2018, 14:23:54 UTC |
ddd41ae | Cécile BARITEL-RUET | 20 December 2018, 13:14:22 UTC | Merge branch '1.0' into deploy-fmatch | 20 December 2018, 13:14:22 UTC |
b2b7e5b | Cécile BARITEL-RUET | 20 December 2018, 13:13:35 UTC | fix List.ec | 20 December 2018, 13:13:35 UTC |
0818e20 | Cécile BARITEL-RUET | 20 December 2018, 12:29:19 UTC | Merge branch '1.0' into deploy-fmatch | 20 December 2018, 12:29:19 UTC |
532e12b | Cécile BARITEL-RUET | 20 December 2018, 12:28:06 UTC | fix types of an operator when its definition is a match, where its type was only its return type inside its body. | 20 December 2018, 12:28:06 UTC |
4a4be28 | Cécile BARITEL-RUET | 20 December 2018, 12:26:49 UTC | . | 20 December 2018, 12:26:49 UTC |
9e29c37 | Cécile BARITEL-RUET | 19 December 2018, 18:00:37 UTC | fix a bug where a meta variable was transformed into a simple local formula. | 19 December 2018, 18:00:37 UTC |
6690416 | Cécile BARITEL-RUET | 19 December 2018, 17:32:05 UTC | . | 19 December 2018, 17:32:05 UTC |
177ec4a | Cécile BARITEL-RUET | 19 December 2018, 17:31:11 UTC | Merge branch '1.0' into deploy-fmatch | 19 December 2018, 17:31:11 UTC |
192a23f | Cécile BARITEL-RUET | 19 December 2018, 17:24:55 UTC | fix type of pred1 from 'a -> bool to 'a -> 'a -> bool | 19 December 2018, 17:24:55 UTC |
f0ceb48 | Cécile BARITEL-RUET | 19 December 2018, 17:24:02 UTC | . | 19 December 2018, 17:24:02 UTC |
0217505 | Cécile BARITEL-RUET | 19 December 2018, 16:58:50 UTC | fix previous fix, now it only changes the order of the reduction | 19 December 2018, 16:58:50 UTC |
c8f2dc2 | Cécile BARITEL-RUET | 19 December 2018, 16:48:55 UTC | fix reduction strategy to not reduce inside a Papp if the other side is only a local/op + add more verbose options | 19 December 2018, 16:48:55 UTC |
95f336c | Cécile BARITEL-RUET | 19 December 2018, 16:19:31 UTC | factoring both Papp to only one + adding a flag to Papp about higher order | 19 December 2018, 16:19:31 UTC |
6a52f1b | Cécile BARITEL-RUET | 19 December 2018, 12:10:55 UTC | fix bug where higher order was after structural matching of application | 19 December 2018, 12:10:55 UTC |
7a10611 | Cécile BARITEL-RUET | 18 December 2018, 17:12:13 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 18 December 2018, 17:12:13 UTC |
930b1b5 | Cécile BARITEL-RUET | 18 December 2018, 17:11:51 UTC | . | 18 December 2018, 17:11:51 UTC |
0b59cac | Pierre-Yves Strub | 18 December 2018, 14:34:23 UTC | fix bug in LDecl where the type of the operator was not correct. | 18 December 2018, 14:35:55 UTC |
fa8c022 | Pierre-Yves Strub | 18 December 2018, 14:34:23 UTC | fix bug in LDecl where the type of the operator was not correct. | 18 December 2018, 14:34:23 UTC |
de4c03e | Pierre-Yves Strub | 18 December 2018, 14:32:48 UTC | partially revert 1497515915108b7ee0f5e5065c0b69511c9383fb | 18 December 2018, 14:32:48 UTC |
1497515 | Cécile BARITEL-RUET | 18 December 2018, 14:26:53 UTC | fix bug in LDecl where the type of the operator was not correct. | 18 December 2018, 14:26:53 UTC |
825ebc2 | Cécile BARITEL-RUET | 17 December 2018, 14:51:57 UTC | fix bug where OGTmem None was tested not equal to OGTmem None. | 17 December 2018, 14:51:57 UTC |
394b4c5 | Cécile BARITEL-RUET | 17 December 2018, 14:34:44 UTC | Merge branch '1.0' into deploy-fmatch | 17 December 2018, 14:34:44 UTC |
88a87da | Cécile BARITEL-RUET | 17 December 2018, 14:33:18 UTC | Merge branch '1.0' of https://github.com/EasyCrypt/easycrypt into 1.0 | 17 December 2018, 14:33:18 UTC |
dfe37eb | Cécile BARITEL-RUET | 17 December 2018, 14:32:33 UTC | fix bug where the type of pred1 was bool instead of 'a -> bool | 17 December 2018, 14:32:33 UTC |
4543274 | Cécile BARITEL-RUET | 17 December 2018, 14:31:38 UTC | . | 17 December 2018, 14:31:38 UTC |
1563ffc | Cécile BARITEL-RUET | 14 December 2018, 11:53:13 UTC | fix bug | 14 December 2018, 11:53:13 UTC |
815daf3 | Cécile BARITEL-RUET | 14 December 2018, 11:32:55 UTC | fix bug + pattern are always typed | 14 December 2018, 11:32:55 UTC |
5a31709 | Benjamin Gregoire | 12 December 2018, 17:00:34 UTC | simplify proof | 12 December 2018, 17:00:34 UTC |
179fc9b | Cécile BARITEL-RUET | 12 December 2018, 14:19:21 UTC | without printing. | 12 December 2018, 14:19:21 UTC |
a84f754 | Cécile BARITEL-RUET | 12 December 2018, 14:16:50 UTC | fix bug where the type of an application was assigned to its operator. | 12 December 2018, 14:16:50 UTC |
17eced8 | Pierre-Yves Strub | 11 December 2018, 16:29:13 UTC | Simplifying async-while examples | 11 December 2018, 16:29:13 UTC |
2d05f8b | Pierre-Yves Strub | 11 December 2018, 16:24:53 UTC | async-while: example for nested loops | 11 December 2018, 16:24:53 UTC |