| f06610a | Kenji Maillard | 31 January 2020, 14:10:31 UTC | do not capture the exceptions of the continuation | 11 February 2020, 09:31:09 UTC |
| 7647d8c | SimonBoulier | 31 January 2020, 16:49:13 UTC | Split the hudge utils.v | 07 February 2020, 22:24:32 UTC |
| e8775e7 | SimonBoulier | 31 January 2020, 15:34:02 UTC | Remove deprecated stuffs | 31 January 2020, 16:26:07 UTC |
| 83c77fe | SimonBoulier | 31 January 2020, 12:36:22 UTC | Remove dependency of pcuic over checker | 31 January 2020, 16:26:07 UTC |
| 778f636 | Théo Winterhalter | 22 January 2020, 20:22:40 UTC | Merge pull request #364 from MetaCoq/refactor_conversion2 Refactor conversion and cie | 22 January 2020, 20:22:40 UTC |
| 14364b5 | SimonBoulier | 22 January 2020, 15:38:14 UTC | Refactor conversion and cie | 22 January 2020, 15:38:14 UTC |
| 37dc18a | Vadim Zaliva | 20 December 2019, 23:57:07 UTC | allow patterns in `mlet` allows to write: ``` '(a,b) <- foo ;; ``` instead of ``` c <- foo ;; let '(a,b) := c in ``` | 06 January 2020, 08:45:46 UTC |
| ee59571 | Théo Winterhalter | 21 December 2019, 14:17:03 UTC | Merge pull request #363 from MetaCoq/context-closure About context closure and reduction | 21 December 2019, 14:17:03 UTC |
| 5a7f502 | Théo Winterhalter | 21 December 2019, 13:14:07 UTC | Set default goal selector to ! in PCUICReduction | 21 December 2019, 13:14:07 UTC |
| 056ed00 | Théo Winterhalter | 21 December 2019, 13:00:21 UTC | Define top-level reduction and show it's included in red1 | 21 December 2019, 13:00:21 UTC |
| 5aeaa5b | Théo Winterhalter | 21 December 2019, 08:54:59 UTC | Define context closure | 21 December 2019, 08:54:59 UTC |
| 2c957aa | Théo Winterhalter | 20 December 2019, 13:14:36 UTC | Merge pull request #358 from MetaCoq/more-eta Properties on η | 20 December 2019, 13:14:36 UTC |
| 50376e1 | Théo Winterhalter | 20 December 2019, 12:42:57 UTC | Fix compilation after new isFixApp | 20 December 2019, 12:42:57 UTC |
| c93ebfe | Théo Winterhalter | 19 December 2019, 13:20:19 UTC | Fix links to examples in README | 19 December 2019, 13:20:19 UTC |
| 9e3badb | Théo Winterhalter | 16 December 2019, 14:03:16 UTC | Attempt to state and prove postponement | 16 December 2019, 14:03:16 UTC |
| 5563fcb | Théo Winterhalter | 12 December 2019, 15:33:27 UTC | Merge pull request #361 from flupe/fresh_universe Added opaque fresh_level | 12 December 2019, 15:33:27 UTC |
| d515627 | flupe | 12 December 2019, 15:07:55 UTC | added opaque fresh_level | 12 December 2019, 15:09:31 UTC |
| 7a7f5b2 | SimonBoulier | 09 December 2019, 16:18:29 UTC | Unify [rdestruct]s | 10 December 2019, 10:45:27 UTC |
| a3105b9 | SimonBoulier | 09 December 2019, 16:00:06 UTC | Move tactic and lemmas about squash | 10 December 2019, 10:45:27 UTC |
| 9f40e20 | SimonBoulier | 09 December 2019, 15:10:41 UTC | Remove a warning | 10 December 2019, 10:45:27 UTC |
| 5ea12e2 | SimonBoulier | 09 December 2019, 14:44:05 UTC | Rename reds_case and app_reds_r | 10 December 2019, 10:45:27 UTC |
| 0977be9 | SimonBoulier | 09 December 2019, 14:37:56 UTC | Implicit arguments for nil | 10 December 2019, 10:45:27 UTC |
| 67d92a1 | SimonBoulier | 09 December 2019, 14:26:19 UTC | Remove duplicate term_forall_list_rec | 10 December 2019, 10:45:27 UTC |
| 8874fb9 | SimonBoulier | 09 December 2019, 10:38:03 UTC | Remove the file Monad.v and use more monadic notation | 09 December 2019, 11:46:23 UTC |
| 62a65a5 | Théo Winterhalter | 07 December 2019, 23:40:22 UTC | Prove inverted induction principle on stacks | 07 December 2019, 23:40:22 UTC |
| 43d0570 | Théo Winterhalter | 06 December 2019, 12:32:23 UTC | Merge pull request #357 from MetaCoq/eta-subst Prove substitution for η | 06 December 2019, 12:32:23 UTC |
| dbb9a29 | Théo Winterhalter | 05 December 2019, 17:09:11 UTC | Prove substitution for η | 05 December 2019, 17:09:11 UTC |
| 00e8bc0 | Théo Winterhalter | 05 December 2019, 15:18:29 UTC | Merge pull request #355 from MetaCoq/eta-spec Define η-equality | 05 December 2019, 15:18:29 UTC |
| 09703d9 | Théo Winterhalter | 03 December 2019, 16:38:18 UTC | Add η-expansion to cumul I have left some TODOs for later. | 05 December 2019, 10:26:46 UTC |
| b7b9d56 | Théo Winterhalter | 04 December 2019, 17:56:28 UTC | Merge pull request #356 from flupe/coq-8.9 Adding Binary Parametricity Translation | 04 December 2019, 17:56:28 UTC |
| 3f14a89 | flupe | 15 October 2019, 13:04:59 UTC | added binary parametricity translation | 04 December 2019, 17:14:15 UTC |
| 5f84587 | Théo Winterhalter | 03 December 2019, 16:15:27 UTC | Fix extraction of eta_expands Plus some import fixes. | 03 December 2019, 16:30:21 UTC |
| 088c8f7 | Théo Winterhalter | 03 December 2019, 14:00:53 UTC | Define η-equality | 03 December 2019, 14:27:18 UTC |
| f4a2643 | Théo Winterhalter | 03 December 2019, 13:51:11 UTC | Merge pull request #354 from MetaCoq/stacks Add LetIn stacks and positions | 03 December 2019, 13:51:11 UTC |
| cd617cb | Théo Winterhalter | 03 December 2019, 10:47:44 UTC | Add LetIn stacks and positions | 03 December 2019, 13:16:59 UTC |
| 71dd547 | Théo Winterhalter | 03 December 2019, 10:29:26 UTC | Merge pull request #353 from MetaCoq/fix-red Reduction of fix now whnf | 03 December 2019, 10:29:26 UTC |
| 97c473e | Théo Winterhalter | 03 December 2019, 09:38:49 UTC | Reduction of fix now whnf | 03 December 2019, 09:38:49 UTC |
| 681e11f | Matthieu Sozeau | 30 November 2019, 15:13:00 UTC | Merge pull request #352 from MetaCoq/iserasable-in-coq One opaque proof shouldn't be opaque | 30 November 2019, 15:13:00 UTC |
| 0d92670 | Matthieu Sozeau | 30 November 2019, 14:20:23 UTC | One opaque proof shouldn't be opaque | 30 November 2019, 14:44:55 UTC |
| a202856 | Matthieu Sozeau | 29 November 2019, 14:24:43 UTC | Merge pull request #350 from MetaCoq/iserasable-in-coq Erasure running in Coq by fueling Acc proofs | 29 November 2019, 14:24:43 UTC |
| d017ff6 | Matthieu Sozeau | 29 November 2019, 01:41:53 UTC | Allow to run retype-checking and erasure in Coq by fueling the Acc proofs Tests working | 29 November 2019, 11:32:41 UTC |
| 62f9b80 | Matthieu Sozeau | 28 November 2019, 15:06:04 UTC | Merge pull request #349 from MetaCoq/safe-envcheck-env Fix safe checker error handling to return the currently verified env | 28 November 2019, 15:06:04 UTC |
| 14407c5 | Matthieu Sozeau | 26 November 2019, 06:21:04 UTC | Fix safe checker error handling to return the currently verified env | 26 November 2019, 06:21:04 UTC |
| f96fa3c | Théo Winterhalter | 22 November 2019, 10:26:08 UTC | Merge pull request #346 from MetaCoq/fix-conv Fix conversion for fix | 22 November 2019, 10:26:08 UTC |
| 8890681 | Théo Winterhalter | 22 November 2019, 08:20:24 UTC | Move things around | 22 November 2019, 09:56:11 UTC |
| e477618 | Théo Winterhalter | 21 November 2019, 17:16:53 UTC | Complete conversion of fixpoints | 21 November 2019, 17:16:53 UTC |
| 0561c0c | Théo Winterhalter | 21 November 2019, 12:46:36 UTC | Define isconv_fix | 21 November 2019, 12:46:36 UTC |
| a3868a2 | Théo Winterhalter | 21 November 2019, 12:26:41 UTC | Remove todos in isconv_fix They were actually not necessary, two fixpoints with a diferent number of functions are just different. | 21 November 2019, 12:29:26 UTC |
| 84cb999 | Théo Winterhalter | 20 November 2019, 17:11:04 UTC | Add isconv_fix_bodies | 20 November 2019, 17:11:04 UTC |
| f58c9b0 | Matthieu Sozeau | 20 November 2019, 12:13:51 UTC | Adapt translations | 20 November 2019, 16:30:06 UTC |
| b8e132d | Matthieu Sozeau | 20 November 2019, 10:43:56 UTC | Adapt test-suite | 20 November 2019, 16:30:06 UTC |
| 2b43057 | Matthieu Sozeau | 20 November 2019, 10:21:05 UTC | Adapt erasure | 20 November 2019, 16:30:06 UTC |
| dbfbfc7 | Matthieu Sozeau | 20 November 2019, 09:50:32 UTC | Update SafeChecker | 20 November 2019, 16:30:06 UTC |
| 2e0bcfe | Matthieu Sozeau | 18 November 2019, 22:36:06 UTC | Adapt PCUIC | 20 November 2019, 16:30:06 UTC |
| 495543b | Matthieu Sozeau | 16 November 2019, 15:16:53 UTC | Change representation of the glob env to an assoc list | 20 November 2019, 16:30:06 UTC |
| 3862244 | Théo Winterhalter | 19 November 2019, 20:25:35 UTC | Define conversion for mfixpoint types | 19 November 2019, 22:12:59 UTC |
| f83378a | SimonBoulier | 18 November 2019, 15:39:56 UTC | Fix compilation for Equations 1.2.1 | 18 November 2019, 16:40:18 UTC |
| 974e6e9 | SimonBoulier | 18 November 2019, 13:36:23 UTC | remove comment | 18 November 2019, 16:40:18 UTC |
| 198220b | SimonBoulier | 08 November 2019, 16:43:44 UTC | type_Case in template + fix compilation | 18 November 2019, 16:40:18 UTC |
| 9cb01de | SimonBoulier | 07 November 2019, 17:14:17 UTC | Fix compilation upto Weakening | 18 November 2019, 16:40:18 UTC |
| 1f45f56 | SimonBoulier | 07 November 2019, 16:19:02 UTC | Change type_Case to remove the useless conversion test | 18 November 2019, 16:40:18 UTC |
| 52d8226 | Théo Winterhalter | 18 November 2019, 12:49:30 UTC | Add positions for going inside mfixpoints Unfortunately we need to rely on strengthening earlier now. | 18 November 2019, 16:26:07 UTC |
| da7f1a6 | Théo Winterhalter | 18 November 2019, 10:46:36 UTC | Merge pull request #344 from MetaCoq/proj-conv Complete conversion of projections | 18 November 2019, 10:46:36 UTC |
| 8cf8136 | Théo Winterhalter | 18 November 2019, 10:06:35 UTC | Update error message | 18 November 2019, 10:06:35 UTC |
| 3e4d8ee | Théo Winterhalter | 18 November 2019, 09:44:25 UTC | Complete conversion of projections | 18 November 2019, 09:44:25 UTC |
| c48137d | Matthieu Sozeau | 16 November 2019, 16:31:23 UTC | Merge pull request #342 from MetaCoq/opam-ci-remove In the ci-opam case, also remove the packages | 16 November 2019, 16:31:23 UTC |
| d18a009 | Matthieu Sozeau | 16 November 2019, 15:18:27 UTC | Fix opam command | 16 November 2019, 15:18:27 UTC |
| ffc58c6 | Matthieu Sozeau | 16 November 2019, 14:28:38 UTC | In the ci-opam case, also remove the packages This avoids confusing the opam cache, which might think it does not have to recompile some packages | 16 November 2019, 14:29:30 UTC |
| 74eabca | nicolas tabareau | 15 November 2019, 09:48:48 UTC | Merge pull request #341 from MetaCoq/remove-JMeq_eq-in-utils remove JMeq_eq by not using depelim or dependent destruction | 15 November 2019, 09:48:48 UTC |
| 0a9f07e | nicolas tabareau | 15 November 2019, 08:50:52 UTC | remove JMeq_eq by not using depelim or dependent destruction when required | 15 November 2019, 08:50:52 UTC |
| d0c8182 | Matthieu Sozeau | 14 November 2019, 18:32:28 UTC | Merge pull request #340 from MetaCoq/fix-primproj-quote Fix the quotation of primitive projections which was repeating inductive decls | 14 November 2019, 18:32:28 UTC |
| c0da9c7 | Matthieu Sozeau | 14 November 2019, 17:23:24 UTC | Fix the quotation of primitive projections which was repeating inductive decls | 14 November 2019, 17:29:25 UTC |
| db80f87 | Matthieu Sozeau | 14 November 2019, 16:41:02 UTC | Finish proof of context conversion, now axiom free (almost, JMeq_eq still) (#339) * Finish proof of context conversion, now axiom free (almost, JMeq_eq still) * Refactor proofs | 14 November 2019, 16:41:02 UTC |
| c835f87 | Matthieu Sozeau | 12 November 2019, 22:19:04 UTC | Fix for equations 1.2.1 (#338) * Fix reliance on global export of `Set Keyed Unification` from Equations 1.2. Makes the code work with Equations.1.2.1 * Update Equations to 1.2.1 on travis. * The checker already depends on equations (depelim) * tauto also relies on Keyed Unification * EArities depends on Keyed Unification too | 12 November 2019, 22:19:04 UTC |
| 66524a4 | Théo Winterhalter | 10 November 2019, 09:43:19 UTC | Merge pull request #337 from MetaCoq/no-focus Set default goal selector to none | 10 November 2019, 09:43:19 UTC |
| 1bb4303 | Théo Winterhalter | 09 November 2019, 22:34:16 UTC | Set default goal selector to none in SafeReduce and Conversion | 09 November 2019, 22:52:23 UTC |
| e02acbc | Théo Winterhalter | 09 November 2019, 16:35:41 UTC | Set default goal selector to none in SafeLemmata | 09 November 2019, 16:46:34 UTC |
| 2f76146 | Théo Winterhalter | 09 November 2019, 13:28:35 UTC | Merge pull request #336 from MetaCoq/omega-eradication Replace omega with lia | 09 November 2019, 13:28:35 UTC |
| 844678e | Théo Winterhalter | 09 November 2019, 10:00:14 UTC | Replace omega with lia As per #327 | 09 November 2019, 12:22:37 UTC |
| a4dec0e | Théo Winterhalter | 09 November 2019, 09:29:34 UTC | Merge pull request #335 from MetaCoq/conversion-case Fix pattern-matching conversion | 09 November 2019, 09:29:34 UTC |
| 6b307aa | Théo Winterhalter | 09 November 2019, 08:40:14 UTC | Move conversion lemmata to PCUICConversion | 09 November 2019, 08:56:47 UTC |
| 3ef2d23 | Théo Winterhalter | 09 November 2019, 08:34:15 UTC | Prove conv_Case_brs | 09 November 2019, 08:34:15 UTC |
| b96bc0f | Théo Winterhalter | 09 November 2019, 08:25:06 UTC | Prove conv_Case_one_brs | 09 November 2019, 08:25:06 UTC |
| 43ac381 | Théo Winterhalter | 08 November 2019, 22:06:11 UTC | Wait for new type_Case to go further | 08 November 2019, 22:06:11 UTC |
| d5e6bf3 | Théo Winterhalter | 08 November 2019, 20:30:49 UTC | Ignore eqdepFacts.ml(i) | 08 November 2019, 20:30:49 UTC |
| d969d9b | Théo Winterhalter | 08 November 2019, 15:14:28 UTC | Now check branches for conversion in case conversion | 08 November 2019, 17:17:23 UTC |
| c062c93 | Théo Winterhalter | 07 November 2019, 18:48:02 UTC | Towards fixing pattern-matching conversion | 07 November 2019, 21:05:26 UTC |
| 2323743 | Théo Winterhalter | 07 November 2019, 15:08:42 UTC | Merge pull request #333 from MetaCoq/conversion-errors Add errors in conversion | 07 November 2019, 15:08:42 UTC |
| 03d3826 | Théo Winterhalter | 07 November 2019, 14:41:22 UTC | More contexts to print_term | 07 November 2019, 14:41:22 UTC |
| aa463c8 | Théo Winterhalter | 07 November 2019, 13:01:00 UTC | Add contexts to error printing | 07 November 2019, 13:01:00 UTC |
| 0ad081a | Théo Winterhalter | 07 November 2019, 10:22:19 UTC | Use Pretty to print terms This is only WIP because we don't handle contexts yet. | 07 November 2019, 10:59:30 UTC |
| e6040c1 | Théo Winterhalter | 06 November 2019, 19:53:42 UTC | Use ConversionResult at the interface and update printing Printing is still WIP. | 06 November 2019, 20:52:27 UTC |
| eff6707 | Théo Winterhalter | 06 November 2019, 16:39:47 UTC | Add errors in conversion | 06 November 2019, 17:59:55 UTC |
| b38c87b | Théo Winterhalter | 02 November 2019, 17:39:22 UTC | Merge pull request #331 from MetaCoq/template-to-pcuic Template to PCUIC | 02 November 2019, 17:39:22 UTC |
| 9b846aa | Théo Winterhalter | 02 November 2019, 09:10:33 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.9' into template-to-pcuic | 02 November 2019, 09:10:33 UTC |
| d4ef631 | Théo Winterhalter | 02 November 2019, 09:10:09 UTC | Minor formatting | 02 November 2019, 09:10:09 UTC |
| 72d088b | Théo Winterhalter | 01 November 2019, 12:10:04 UTC | Update red1 on tFix and tCoFix in Template + complete trans_red1 | 01 November 2019, 12:36:18 UTC |
| 964126a | Théo Winterhalter | 01 November 2019, 11:30:44 UTC | Update red1 on tCase in Template From this we remove another admit in Template to PCUIC | 01 November 2019, 11:30:44 UTC |
| 853c15a | Théo Winterhalter | 30 October 2019, 18:18:19 UTC | Fix eq_term in Template and prove trans_eq_term_upto_univ | 30 October 2019, 18:18:37 UTC |
| 50d59be | Théo Winterhalter | 30 October 2019, 17:52:18 UTC | Prove trans_eq_term | 30 October 2019, 17:52:18 UTC |
