| 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 |
| 94b8986 | Cécile BARITEL-RUET | 11 December 2018, 16:11:22 UTC | . | 11 December 2018, 16:11:22 UTC |
| b67a33f | Cécile BARITEL-RUET | 11 December 2018, 15:57:23 UTC | without printing | 11 December 2018, 15:57:23 UTC |
| 8b47a55 | Cécile BARITEL-RUET | 11 December 2018, 15:22:47 UTC | fix beta reduction + fix bug where already known meta-var was substitued without going through reduction | 11 December 2018, 15:22:47 UTC |
| 7a8b1d0 | Pierre-Yves Strub | 11 December 2018, 14:10:05 UTC | | 11 December 2018, 14:10:05 UTC |
| 10742eb | Cécile BARITEL-RUET | 11 December 2018, 13:44:34 UTC | EcFMatching : mkengine : first reduction_info is for matching, second is for same meta-variable | 11 December 2018, 13:44:34 UTC |
| d96e542 | Cécile BARITEL-RUET | 11 December 2018, 10:30:31 UTC | . | 11 December 2018, 10:30:31 UTC |
| 729330a | Cécile BARITEL-RUET | 10 December 2018, 14:52:40 UTC | adding eta-reduction. cannot fix no-delta for predC | 10 December 2018, 14:52:40 UTC |
| ff6273d | Cécile BARITEL-RUET | 10 December 2018, 12:33:37 UTC | add case : if pattern reduction gives the same pattern, then don't try again. | 10 December 2018, 12:33:37 UTC |
| f6d7bb8 | Cécile BARITEL-RUET | 10 December 2018, 10:45:44 UTC | fix bug where the type of an application was wrong | 10 December 2018, 10:45:44 UTC |
| 39b142f | Pierre-Yves Strub | 07 December 2018, 09:43:46 UTC | | 07 December 2018, 09:43:50 UTC |
| 18e23f0 | Cécile BARITEL-RUET | 07 December 2018, 09:43:17 UTC | fix some things | 07 December 2018, 09:43:17 UTC |
| 542f817 | Cécile BARITEL-RUET | 07 December 2018, 09:16:46 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 07 December 2018, 09:16:46 UTC |
| 0bf642c | Cécile BARITEL-RUET | 07 December 2018, 09:16:22 UTC | fix nadd_match | 07 December 2018, 09:16:22 UTC |
| 87dd4fd | Pierre-Yves Strub | 06 December 2018, 16:21:22 UTC | | 06 December 2018, 16:21:22 UTC |
| 494b225 | Pierre-Yves Strub | 06 December 2018, 16:05:55 UTC | | 06 December 2018, 16:13:11 UTC |
| 59f83c9 | Pierre-Yves Strub | 06 December 2018, 15:42:23 UTC | | 06 December 2018, 16:12:50 UTC |
| f7b98fe | Pierre-Yves Strub | 06 December 2018, 15:35:52 UTC | | 06 December 2018, 16:12:32 UTC |
| 1f34a0e | Pierre-Yves Strub | 06 December 2018, 14:17:18 UTC | | 06 December 2018, 16:11:39 UTC |
| f7a574e | Cécile BARITEL-RUET | 06 December 2018, 16:06:18 UTC | fix type of pattern_of_memory | 06 December 2018, 16:06:18 UTC |
| 44dc76d | Cécile BARITEL-RUET | 06 December 2018, 16:05:11 UTC | pattern_of_memory | 06 December 2018, 16:05:11 UTC |
| c392978 | Cécile BARITEL-RUET | 06 December 2018, 15:40:05 UTC | pattern_of_form : match_env -> form -> pattern | 06 December 2018, 15:40:05 UTC |
| 4da20f4 | Cécile BARITEL-RUET | 06 December 2018, 15:35:03 UTC | modify pbinding : gty option -> ogty | 06 December 2018, 15:35:03 UTC |
| d252814 | Cécile BARITEL-RUET | 06 December 2018, 11:09:16 UTC | fsubst_of_env : match_env -> env -> f_subst | 06 December 2018, 11:09:16 UTC |
| b9c2b36 | Cécile BARITEL-RUET | 06 December 2018, 10:41:19 UTC | moved eq_tests to a EQ module. + add_meta_var : match_env -> ident -> match_env + union of the meta_vars in the creation of an engine | 06 December 2018, 10:41:19 UTC |
| dc1771a | Cécile BARITEL-RUET | 05 December 2018, 15:23:28 UTC | psubst : match_env -> hyps -> p_subst | 05 December 2018, 15:23:28 UTC |
| eea6dc3 | Cécile BARITEL-RUET | 05 December 2018, 15:14:50 UTC | . | 05 December 2018, 15:14:50 UTC |
| 6d14276 | Cécile BARITEL-RUET | 05 December 2018, 15:10:34 UTC | . | 05 December 2018, 15:10:34 UTC |
| a16caab | Cécile BARITEL-RUET | 05 December 2018, 14:07:12 UTC | removed a fprintf that halts easycrypt's answer... | 05 December 2018, 14:07:12 UTC |
| 6b3adf9 | Cécile BARITEL-RUET | 05 December 2018, 13:50:43 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 05 December 2018, 13:50:43 UTC |
| 66ca8a2 | Cécile BARITEL-RUET | 05 December 2018, 13:48:44 UTC | + match_env : { unienv ; pattern Mid.t ; Sid.t } - remove dead code in Psusbt + modify matching alg to work with match_env | 05 December 2018, 13:48:44 UTC |
| 8d7f084 | Pierre-Yves Strub | 05 December 2018, 12:30:42 UTC | | 05 December 2018, 12:30:47 UTC |
| 091eda8 | Cécile BARITEL-RUET | 05 December 2018, 12:29:50 UTC | + match_is_full : environment -> bool | 05 December 2018, 12:29:50 UTC |
| dec183f | Cécile BARITEL-RUET | 05 December 2018, 12:16:11 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 05 December 2018, 12:16:11 UTC |
| 2bae038 | Cécile BARITEL-RUET | 05 December 2018, 12:16:03 UTC | . | 05 December 2018, 12:16:03 UTC |
| a4b7d5c | Pierre-Yves Strub | 05 December 2018, 10:36:10 UTC | refactoring | 05 December 2018, 10:36:10 UTC |
| 362e1f0 | Cécile BARITEL-RUET | 04 December 2018, 11:06:57 UTC | fix bug where matching did not enter a bd_Hoare formula (an other cases) | 04 December 2018, 11:06:57 UTC |
| c9daace | Cécile BARITEL-RUET | 04 December 2018, 10:23:52 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 04 December 2018, 10:23:52 UTC |
| bff13e3 | Cécile BARITEL-RUET | 04 December 2018, 10:22:44 UTC | fix complexity bug | 04 December 2018, 10:22:44 UTC |
| 2a44ddc | Pierre-Yves Strub | 03 December 2018, 16:30:39 UTC | | 03 December 2018, 16:30:39 UTC |
| f99ec8c | Cécile BARITEL-RUET | 03 December 2018, 15:56:44 UTC | . | 03 December 2018, 15:56:44 UTC |
| 63372b6 | Cécile BARITEL-RUET | 03 December 2018, 15:29:20 UTC | . | 03 December 2018, 15:29:20 UTC |
| a59bdeb | Cécile BARITEL-RUET | 03 December 2018, 15:26:38 UTC | . | 03 December 2018, 15:26:38 UTC |
| 54dbd76 | Cécile BARITEL-RUET | 03 December 2018, 15:16:45 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 03 December 2018, 15:16:45 UTC |
| dabe245 | Cécile BARITEL-RUET | 03 December 2018, 15:12:49 UTC | final substitution of all the unified types | 03 December 2018, 15:12:49 UTC |
| a37b9f4 | Cécile BARITEL-RUET | 03 December 2018, 15:05:33 UTC | modified red_strat to red_info -> red_inf -> red_info * red_info modified substitution that substitutes unified types | 03 December 2018, 15:05:33 UTC |
| d852f70 | Pierre-Yves Strub | 03 December 2018, 13:26:23 UTC | fix pose with new API | 03 December 2018, 13:26:23 UTC |
| f4e70bf | Cécile BARITEL-RUET | 03 December 2018, 13:19:15 UTC | form_of_pattern (env -> pattern -> form) raises Invalid_Type when cannot be mactched as a formula | 03 December 2018, 13:19:15 UTC |
| 9d4d649 | Cécile BARITEL-RUET | 03 December 2018, 13:04:06 UTC | Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch | 03 December 2018, 13:04:06 UTC |
| a8043c2 | Cécile BARITEL-RUET | 03 December 2018, 13:03:50 UTC | form_of_pattern : to finish | 03 December 2018, 13:03:50 UTC |
| f936435 | Pierre-Yves Strub | 03 December 2018, 12:40:04 UTC | (internal API) - typed application soft-constructor for forms | 03 December 2018, 12:40:13 UTC |
| ed7bf6c | Pierre-Yves Strub | 03 December 2018, 12:40:04 UTC | (internal API) - typed application soft-constructor for forms | 03 December 2018, 12:40:04 UTC |
| 9a19a0b | Pierre-Yves Strub | 03 December 2018, 10:42:33 UTC | `pose` with new match starts working | 03 December 2018, 10:42:33 UTC |
| 085e6aa | Pierre-Yves Strub | 03 December 2018, 09:40:02 UTC | Merge branch '1.0' into deploy-fmatch | 03 December 2018, 09:40:02 UTC |
| 427b150 | Cécile BARITEL-RUET | 03 December 2018, 08:49:43 UTC | . | 03 December 2018, 08:49:43 UTC |
| 6ea2431 | Cécile BARITEL-RUET | 30 November 2018, 12:28:25 UTC | bug fixes | 30 November 2018, 12:28:25 UTC |
| cd3712f | Cécile BARITEL-RUET | 28 November 2018, 15:28:29 UTC | new version | 28 November 2018, 15:28:29 UTC |
| 3c1cc99 | Cécile BARITEL-RUET | 19 November 2018, 12:34:48 UTC | . | 19 November 2018, 12:34:48 UTC |
| 08e5a8b | Cécile BARITEL-RUET | 16 November 2018, 16:00:22 UTC | pattern reduction when pattern is an axiom + first steps of Psubst | 16 November 2018, 16:00:22 UTC |
| 68a62da | Cécile BARITEL-RUET | 15 November 2018, 13:40:30 UTC | first steps of the reduction | 15 November 2018, 13:40:30 UTC |
| f120f53 | Benjamin Gregoire | 13 November 2018, 08:12:18 UTC | fix error message | 13 November 2018, 08:12:18 UTC |
| 0f53ba6 | Cécile BARITEL-RUET | 12 November 2018, 08:56:54 UTC | implem checks + reduction from reduction_info - when EcUnify.unify fails, the unienv is restored (copy created, then stored if no backup was previously there) - implements a reduction function : reduction_info -> reduction strategy, that only reduce forms in the right | 12 November 2018, 08:56:54 UTC |
| 9959602 | Pierre-Yves Strub | 07 November 2018, 21:51:34 UTC | More results in ZModP | 07 November 2018, 21:51:34 UTC |
| 5c95527 | Pierre-Yves Strub | 07 November 2018, 21:45:42 UTC | New tactic: - exlim (shorthand for exists*; elim*) - ecall (seq + exlim + call with inference) | 07 November 2018, 21:47:02 UTC |
| d043056 | Cécile BARITEL-RUET | 06 November 2018, 13:07:32 UTC | very little fix | 06 November 2018, 13:07:32 UTC |
| cf00160 | Cécile BARITEL-RUET | 06 November 2018, 13:01:47 UTC | not so pretty printer for patterns | 06 November 2018, 13:01:47 UTC |
| 22c70a2 | Cécile BARITEL-RUET | 30 October 2018, 16:06:39 UTC | higher order patterns are recognized, but rewriting higher order does not work | 30 October 2018, 16:06:39 UTC |
| 28c5228 | Pierre-Yves Strub | 25 October 2018, 15:21:38 UTC | Fix Cramer Shoup | 25 October 2018, 15:21:38 UTC |
