| b960d7d | Matthieu Sozeau | 03 March 2020, 15:30:31 UTC | Fixed univ.v issue | 10 March 2020, 13:36:59 UTC |
| f698673 | SimonBoulier | 07 February 2020, 22:27:35 UTC | Big change in universes: - change the representation of UnivExpr - change the representation of universes (sorted, non empty list w/o duplicate) - prove completness of the comparison algorithm | 04 March 2020, 11:38:55 UTC |
| e4d4e80 | Théo Winterhalter | 02 March 2020, 09:17:23 UTC | Merge pull request #380 from MetaCoq/testsuite-tsl Fix minor stuffs in test-suite and translations | 02 March 2020, 09:17:23 UTC |
| d4cac4d | SimonBoulier | 02 March 2020, 08:22:11 UTC | Fix minor stuffs in test-suite and translations | 02 March 2020, 08:22:11 UTC |
| ffe5f7b | Matthieu Sozeau | 28 February 2020, 11:20:52 UTC | Update README.md | 28 February 2020, 11:20:52 UTC |
| 0653ec4 | Matthieu Sozeau | 27 February 2020, 11:42:00 UTC | Update opam files | 27 February 2020, 11:42:00 UTC |
| 6aa7b3f | Matthieu Sozeau | 27 February 2020, 11:01:39 UTC | Fix travis script in case switch exists | 27 February 2020, 11:01:39 UTC |
| d63f7c4 | Matthieu Sozeau | 27 February 2020, 10:50:19 UTC | Update test-suite to 8.10 | 27 February 2020, 10:50:19 UTC |
| 606653e | Matthieu Sozeau | 26 February 2020, 19:57:35 UTC | No more camlp5 needed! | 26 February 2020, 19:57:35 UTC |
| 71d047b | Matthieu Sozeau | 26 February 2020, 19:50:35 UTC | Fix issue with change of switch | 26 February 2020, 19:50:35 UTC |
| b6040f8 | Matthieu Sozeau | 26 February 2020, 19:37:43 UTC | Update trarvis requirements to 8.10 | 26 February 2020, 19:37:43 UTC |
| 1b207b0 | Matthieu Sozeau | 26 February 2020, 19:30:26 UTC | Fix trarnslations. This required reverting the hack of "mind_body_to_entry" to compute parameters. | 26 February 2020, 19:30:26 UTC |
| cb5275f | Matthieu Sozeau | 14 February 2020, 16:07:13 UTC | Disable plugin building in checker also | 14 February 2020, 16:07:13 UTC |
| d404665 | Matthieu Sozeau | 14 February 2020, 15:45:19 UTC | Update .gitignore | 14 February 2020, 15:45:19 UTC |
| 9c5fb71 | Matthieu Sozeau | 14 February 2020, 15:43:01 UTC | Ported erasure | 14 February 2020, 15:43:01 UTC |
| 76b5517 | Matthieu Sozeau | 14 February 2020, 15:27:38 UTC | Ported the safe checker | 14 February 2020, 15:27:38 UTC |
| aa9a5ef | Matthieu Sozeau | 14 February 2020, 14:35:56 UTC | Update PCUIC to 8.10, remove plugin construction | 14 February 2020, 14:35:56 UTC |
| b3e520d | Matthieu Sozeau | 14 February 2020, 14:11:10 UTC | Adapt .v files to 8.10 | 14 February 2020, 14:11:10 UTC |
| 431dfc3 | Matthieu Sozeau | 14 February 2020, 13:27:20 UTC | Induction.ml not needed for extraction of template-coq anymore | 14 February 2020, 13:27:20 UTC |
| e850060 | Matthieu Sozeau | 14 February 2020, 13:25:24 UTC | Move .ml4's to .mlg's | 14 February 2020, 13:25:24 UTC |
| 9b2ab6f | Matthieu Sozeau | 14 February 2020, 13:17:23 UTC | Extractable compiling too | 14 February 2020, 13:17:23 UTC |
| 01a465f | Matthieu Sozeau | 13 February 2020, 15:53:13 UTC | Finally running the loader! | 13 February 2020, 15:53:13 UTC |
| bdae782 | Matthieu Sozeau | 13 February 2020, 14:04:38 UTC | WIP Porting to 8.10 | 13 February 2020, 14:04:38 UTC |
| a7a55ad | Matthieu Sozeau | 11 February 2020, 16:36:30 UTC | WIP adapting to 8.10 | 11 February 2020, 16:36:30 UTC |
| c471531 | Matthieu Sozeau | 11 February 2020, 15:35:25 UTC | Port to Coq 8.10 (not supporting SProp or Int) | 11 February 2020, 15:35:25 UTC |
| 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 |
