| 659de9d | SimonBoulier | 07 November 2019, 15:13:07 UTC | [WIP] Compile jusque extraction sauf plugin | 07 November 2019, 15:13:07 UTC |
| 293c040 | SimonBoulier | 06 November 2019, 16:30:48 UTC | [WIP] bug in conversion in test with conv_context in check_correct_arity | 07 November 2019, 12:13:52 UTC |
| f098d84 | SimonBoulier | 07 November 2019, 12:13:13 UTC | Fixing compilation | 07 November 2019, 12:13:13 UTC |
| cb485b9 | SimonBoulier | 02 November 2019, 21:35:59 UTC | WIP correct check_correct_arity to PCUIC | 02 November 2019, 21:35:59 UTC |
| cfe8f12 | SimonBoulier | 02 November 2019, 13:47:15 UTC | correct check_correct_arity in Template | 02 November 2019, 13:47:15 UTC |
| 5fd5347 | SimonBoulier | 02 November 2019, 09:05:33 UTC | Refactor conversion. Conversion is no longer the cumulativity in both directions. Now [conv] refers to the old [conv_alt]. Also the second [conv] has been renamed [conv_cum] (it is only used for safe conversion checker). | 02 November 2019, 10:15:42 UTC |
| b288de7 | Théo Winterhalter | 30 October 2019, 07:15:57 UTC | Merge pull request #330 from MetaCoq/template-to-pcuic Repairing TemplateCoq to PCUIC (Updating typing rules) | 30 October 2019, 07:15:57 UTC |
| 27778e8 | Théo Winterhalter | 29 October 2019, 21:58:54 UTC | Rehab typing_wf_sigma modulo on_global_env_mix | 29 October 2019, 21:58:54 UTC |
| d8b8f0b | Théo Winterhalter | 29 October 2019, 21:34:21 UTC | Fix substitution lemma for Template | 29 October 2019, 21:34:21 UTC |
| f878e15 | Théo Winterhalter | 29 October 2019, 21:24:12 UTC | Prove substitution for types_of_case | 29 October 2019, 21:24:12 UTC |
| a361ee4 | Théo Winterhalter | 29 October 2019, 16:39:30 UTC | [WIP] Update typing of TemplateCoq to match PCUIC | 29 October 2019, 16:58:32 UTC |
| d87ea3a | Théo Winterhalter | 29 October 2019, 16:22:10 UTC | Merge pull request #328 from MetaCoq/env-typing-functor Functorisation of environment typing | 29 October 2019, 16:22:10 UTC |
| 74c00a7 | Théo Winterhalter | 29 October 2019, 14:24:47 UTC | Complete update of pcuic and erasure | 29 October 2019, 15:34:32 UTC |
| 85d3fad | Théo Winterhalter | 29 October 2019, 12:15:15 UTC | Update pcuic after functorisation of declarations typing | 29 October 2019, 12:15:15 UTC |
| 570728f | Théo Winterhalter | 29 October 2019, 10:46:53 UTC | Remove axioms from Functor as they cannot be extracted | 29 October 2019, 10:46:53 UTC |
| b413d6f | Théo Winterhalter | 28 October 2019, 16:22:53 UTC | Functorise declaration typing I added some admits, and proved some stuff that wasn't needed before. Hopefully the admits will go away when I make TemplateCoq match PCUIC. | 29 October 2019, 09:35:25 UTC |
| 0107d5e | Théo Winterhalter | 28 October 2019, 14:16:17 UTC | Update post functorisation For instance some `tSort` become `PCUICTerm.tSort` which has to be unfolded. | 28 October 2019, 14:16:17 UTC |
| 9d5b10a | Théo Winterhalter | 28 October 2019, 13:31:48 UTC | Ignore pcuic/Makefile.plugin-e | 28 October 2019, 13:31:48 UTC |
| 29fc59d | Théo Winterhalter | 28 October 2019, 13:30:30 UTC | Add EnvTyping to functor | 28 October 2019, 13:30:30 UTC |
| 405a60f | Théo Winterhalter | 28 October 2019, 10:51:02 UTC | Move consistent_instance to functor | 28 October 2019, 10:51:02 UTC |
| 05b64e8 | Théo Winterhalter | 28 October 2019, 09:08:20 UTC | Move prop_global_ext_levels to functor | 28 October 2019, 09:08:20 UTC |
| 36878ea | Théo Winterhalter | 28 October 2019, 08:47:54 UTC | Move on_udecl and such to functor | 28 October 2019, 08:47:54 UTC |
| 995bbd0 | Théo Winterhalter | 27 October 2019, 21:28:30 UTC | Fix extraction of EnvironmentTyping | 27 October 2019, 21:28:30 UTC |
| 3ae0870 | Théo Winterhalter | 27 October 2019, 19:30:35 UTC | Duplicate Environment functor as funsig with Include | 27 October 2019, 19:30:35 UTC |
| f56db8c | Théo Winterhalter | 25 October 2019, 20:48:45 UTC | Functorise lookup of global env | 25 October 2019, 20:48:45 UTC |
| 010ebfe | SimonBoulier | 24 October 2019, 15:34:49 UTC | Fix compilation | 24 October 2019, 16:31:45 UTC |
| 2b43f3a | SimonBoulier | 24 October 2019, 13:32:20 UTC | Fix compilation | 24 October 2019, 16:31:45 UTC |
| c8ca6e1 | SimonBoulier | 24 October 2019, 08:34:33 UTC | Create directory examples and clean in tauto | 24 October 2019, 16:31:45 UTC |
| 777cbd5 | Théo Winterhalter | 24 October 2019, 10:17:10 UTC | Use functors to factorise environments (#324) * [WIP] Use functors to factorise environments * Add Environment to mlpack * Fix compilation after functorisation of environment * Use Environment functor in pcuic as well * Update erasure after adding Environment * Use Include instead of Export * Also factorise global contexts * Make changes after functorisation of global environment * Use old reify for TemplateMonad (quickfix) | 24 October 2019, 10:17:10 UTC |
| 1086391 | nicolas tabareau | 23 October 2019, 17:07:46 UTC | add tauto tactics example | 23 October 2019, 17:07:46 UTC |
| 8f8237a | Théo Winterhalter | 22 October 2019, 13:27:37 UTC | Merge pull request #323 from MetaCoq/minor-changes Minor changes | 22 October 2019, 13:27:37 UTC |
| 9aada59 | Théo Winterhalter | 22 October 2019, 12:44:14 UTC | Backport "clean safechecker_test.v" | 22 October 2019, 12:44:14 UTC |
| f2eb27d | Théo Winterhalter | 22 October 2019, 12:37:15 UTC | Remove one admit in vs.v | 22 October 2019, 12:37:15 UTC |
| 49b0478 | Théo Winterhalter | 22 October 2019, 12:32:27 UTC | Backport "Fix metacoq_safechecker wrong timing" | 22 October 2019, 12:32:27 UTC |
| d4e316c | Théo Winterhalter | 21 October 2019, 18:13:53 UTC | Merge pull request #321 from MetaCoq/arity-again Prove stronger Is_conv_to_Arity_inv | 21 October 2019, 18:13:53 UTC |
| f4157e4 | Théo Winterhalter | 21 October 2019, 15:31:08 UTC | Fix ErasureFunction with updated Is_conv_to_Arity_inv | 21 October 2019, 15:31:08 UTC |
| 4d955bf | Théo Winterhalter | 21 October 2019, 15:23:08 UTC | Prove stronger Is_conv_to_Arity_inv | 21 October 2019, 15:23:08 UTC |
| 301473c | Théo Winterhalter | 21 October 2019, 08:04:01 UTC | Link in README go to other READMEs | 21 October 2019, 08:04:01 UTC |
| 3d6b55b | Théo Winterhalter | 21 October 2019, 08:01:48 UTC | Update safechecker README | 21 October 2019, 08:01:48 UTC |
| 0d1cec3 | Théo Winterhalter | 20 October 2019, 12:08:36 UTC | Use permalink for doc | 20 October 2019, 12:08:36 UTC |
| bdbd188 | Théo Winterhalter | 19 October 2019, 16:21:45 UTC | Tabulate pcuic files | 19 October 2019, 16:21:45 UTC |
| d55c9a1 | Théo Winterhalter | 19 October 2019, 15:38:26 UTC | Update README | 19 October 2019, 15:38:26 UTC |
| c77e451 | Théo Winterhalter | 18 October 2019, 16:11:54 UTC | Merge pull request #318 from MetaCoq/arity-proofs Fix and prove Is_conv_to_Arity_inv | 18 October 2019, 16:11:54 UTC |
| 7e712ab | Théo Winterhalter | 18 October 2019, 15:15:34 UTC | Remove unneeded hyp for inver_cumul_arity_r/l | 18 October 2019, 15:17:38 UTC |
| fde02ff | Théo Winterhalter | 18 October 2019, 15:06:23 UTC | Prove invert_cumul_arity_l | 18 October 2019, 15:06:23 UTC |
| d91a2b2 | Théo Winterhalter | 18 October 2019, 15:04:39 UTC | Prove isArity_subst and isArity_red1 | 18 October 2019, 15:04:39 UTC |
| 4417f89 | Théo Winterhalter | 18 October 2019, 15:01:47 UTC | Almost prove isArity_red1 | 18 October 2019, 15:01:47 UTC |
| 5d877e7 | Théo Winterhalter | 18 October 2019, 10:26:38 UTC | Prove invert_cumul_arity_r modulo isArity_red1 | 18 October 2019, 10:26:38 UTC |
| c5005c9 | Théo Winterhalter | 18 October 2019, 09:27:24 UTC | Fix and prove Is_conv_to_Arity_inv | 18 October 2019, 09:36:22 UTC |
| bf9cf02 | Matthieu Sozeau | 18 October 2019, 09:02:13 UTC | Merge pull request #316 from MetaCoq/remove-program Remove unnecessary uip axioms | 18 October 2019, 09:02:13 UTC |
| 390aedf | Matthieu Sozeau | 18 October 2019, 08:58:25 UTC | Merge pull request #289 from MetaCoq/typing_inds Cleaning in the typing of inductive declarations | 18 October 2019, 08:58:25 UTC |
| 2a0cf24 | SimonBoulier | 18 October 2019, 08:13:59 UTC | Make compiling | 18 October 2019, 08:13:59 UTC |
| edf57d3 | Théo Winterhalter | 18 October 2019, 08:05:10 UTC | Comment out stack overflow generating command | 18 October 2019, 08:05:31 UTC |
| 43c040a | Théo Winterhalter | 18 October 2019, 07:04:56 UTC | Fix eq_refl in translations | 18 October 2019, 07:04:56 UTC |
| d47f1e2 | Théo Winterhalter | 17 October 2019, 20:45:29 UTC | Put back stdlib extraction | 17 October 2019, 20:45:56 UTC |
| fb33796 | Théo Winterhalter | 17 October 2019, 20:25:50 UTC | Fix extraction of checker | 17 October 2019, 20:25:50 UTC |
| 14e4f99 | Théo Winterhalter | 17 October 2019, 16:34:06 UTC | Use Equations everywhere in Checker as well | 17 October 2019, 20:09:00 UTC |
| 88ed804 | Théo Winterhalter | 17 October 2019, 15:37:43 UTC | Require Equations everwhere to make sure | 17 October 2019, 15:43:36 UTC |
| 585737f | Théo Winterhalter | 17 October 2019, 10:09:53 UTC | Use Equation's depelim in pcuic | 17 October 2019, 15:19:13 UTC |
| 776db22 | SimonBoulier | 17 October 2019, 13:14:26 UTC | cleaning | 17 October 2019, 13:14:26 UTC |
| c7b17b4 | SimonBoulier | 19 September 2019, 15:48:45 UTC | Cleaning in the typing of inductive declarations | 17 October 2019, 12:45:22 UTC |
| 3bbf2d3 | Théo Winterhalter | 17 October 2019, 09:50:34 UTC | Ignore PCUICUtils ml | 17 October 2019, 09:50:34 UTC |
| d6932fd | Théo Winterhalter | 17 October 2019, 09:48:46 UTC | Remove problematic test | 17 October 2019, 09:48:46 UTC |
| 4bd2098 | SimonBoulier | 17 October 2019, 09:24:53 UTC | cleaning | 17 October 2019, 09:25:58 UTC |
| 047d086 | Théo Winterhalter | 17 October 2019, 08:20:17 UTC | Add PCUICUtils to extracted libraries | 17 October 2019, 08:20:17 UTC |
| f9bdca8 | Théo Winterhalter | 16 October 2019, 16:33:20 UTC | Remove Eqdep.Eq_rect_eq.eq_rect_eq and more | 16 October 2019, 16:33:20 UTC |
| 9eaf12d | Théo Winterhalter | 16 October 2019, 14:18:53 UTC | wGraph.to_simple is defined using Equations | 16 October 2019, 14:37:59 UTC |
| b7287e0 | Théo Winterhalter | 16 October 2019, 13:42:15 UTC | Load Equations in SafeChecker and TemplateToPCUICCorrectness | 16 October 2019, 13:42:15 UTC |
| 2f9ada2 | Théo Winterhalter | 16 October 2019, 12:56:07 UTC | Use Equations' dependent induction in pcuic | 16 October 2019, 13:23:02 UTC |
| dad8891 | Théo Winterhalter | 16 October 2019, 11:48:13 UTC | Merge pull request #313 from MetaCoq/wellformed_eq_term Removing axioms introduced by #302 | 16 October 2019, 11:48:13 UTC |
| e439ab7 | Théo Winterhalter | 16 October 2019, 08:20:08 UTC | Move lemmata to their rightful place | 16 October 2019, 10:06:22 UTC |
| 86fc9c8 | Théo Winterhalter | 15 October 2019, 20:25:38 UTC | Prove eqb_term_refl | 15 October 2019, 20:25:38 UTC |
| e736a6d | Théo Winterhalter | 15 October 2019, 20:02:32 UTC | Prove eqb_term_upto_univ_refl | 15 October 2019, 20:02:32 UTC |
| 705b85c | Théo Winterhalter | 15 October 2019, 19:52:46 UTC | Almost done with eqb_term_refl | 15 October 2019, 19:52:46 UTC |
| 7d4b3df | Théo Winterhalter | 15 October 2019, 17:43:59 UTC | Prove App_conv' | 15 October 2019, 17:43:59 UTC |
| 2f3833b | Théo Winterhalter | 15 October 2019, 17:38:12 UTC | wellformed_eq_term_upto_univ is no longer needed | 15 October 2019, 17:38:12 UTC |
| 8acb7f1 | Théo Winterhalter | 15 October 2019, 15:41:11 UTC | Remove wellformed_eq_term from tConst case Going for even more symmetry | 15 October 2019, 15:44:24 UTC |
| ed50dd9 | Théo Winterhalter | 14 October 2019, 18:38:03 UTC | Partly prove isWfArity_eq_term_upto_univ | 15 October 2019, 15:15:52 UTC |
| 99860bf | Théo Winterhalter | 14 October 2019, 13:24:29 UTC | Prove destArity_eq_term_upto_univ | 15 October 2019, 15:15:52 UTC |
| ab11aea | Théo Winterhalter | 15 October 2019, 15:15:07 UTC | Merge pull request #315 from MetaCoq/conv-args-coq-8.9-again More symmetric approach to conversion of stacks (again 8.9) | 15 October 2019, 15:15:07 UTC |
| 72cbaa6 | Théo Winterhalter | 26 September 2019, 13:34:58 UTC | Use leq in the leq branch of fallback | 15 October 2019, 14:42:52 UTC |
| b08d5cd | Théo Winterhalter | 15 October 2019, 14:42:48 UTC | Give isconv_args two terms instead of one to account for cumul Removes need for `wellformed_zipc_replace`! | 15 October 2019, 14:42:48 UTC |
| f39bd93 | SimonBoulier | 08 October 2019, 10:47:10 UTC | Add univ_context before safe-checking the toplevel term + remove a source of incompleteness in equality of universes (syntactic equality was not taken in account) | 08 October 2019, 17:13:57 UTC |
| 2a9d854 | SimonBoulier | 08 October 2019, 07:48:53 UTC | check_isWAT instead of check_isType in SafeChecker | 08 October 2019, 17:13:57 UTC |
| 0d0b30f | Théo Winterhalter | 07 October 2019, 07:21:27 UTC | Update gitignore With the same changes again... Stop rebasing! | 07 October 2019, 07:21:27 UTC |
| e099ed5 | Matthieu Sozeau | 27 September 2019, 17:34:04 UTC | Add Danil to the team | 27 September 2019, 17:38:51 UTC |
| 8cecb1b | Matthieu Sozeau | 27 September 2019, 16:26:10 UTC | Add extraction with time bounds reference in the Papers section | 27 September 2019, 16:31:14 UTC |
| cba228c | Matthieu Sozeau | 27 September 2019, 15:46:51 UTC | Typos and add test-suite/*_test.v files for safechecker and erasure | 27 September 2019, 16:01:52 UTC |
| f3ee505 | Matthieu Sozeau | 27 September 2019, 15:14:02 UTC | Update opam files for Coq 8.9 | 27 September 2019, 15:14:02 UTC |
| 9c0ab09 | Matthieu Sozeau | 27 September 2019, 14:50:29 UTC | Rework README.md | 27 September 2019, 15:06:41 UTC |
| 3b6fc70 | Matthieu Sozeau | 27 September 2019, 14:34:35 UTC | Fix README.md | 27 September 2019, 15:04:30 UTC |
| 267f406 | Matthieu Sozeau | 27 September 2019, 14:57:22 UTC | Update .gitignore | 27 September 2019, 14:57:22 UTC |
| e3c587d | Matthieu Sozeau | 27 September 2019, 13:53:15 UTC | Fix vs test-suite example for 8.9 | 27 September 2019, 13:53:15 UTC |
| d9ce847 | Matthieu Sozeau | 27 September 2019, 13:47:47 UTC | Fix local config for building translations and README.md | 27 September 2019, 13:47:47 UTC |
| 30e2b2b | Matthieu Sozeau | 27 September 2019, 13:20:26 UTC | Fixes in README.md | 27 September 2019, 13:25:00 UTC |
| 7ac2083 | Matthieu Sozeau | 27 September 2019, 13:09:07 UTC | Fix after merge | 27 September 2019, 13:09:07 UTC |
| a92eb43 | Matthieu Sozeau | 27 September 2019, 12:22:20 UTC | Merge remote-tracking branch 'origin/coq-8.8' into coq-8.9 | 27 September 2019, 12:22:20 UTC |
| eeeb923 | Matthieu Sozeau | 27 September 2019, 12:07:58 UTC | Update Travis webhook for new gitter channel | 27 September 2019, 12:07:58 UTC |
| c66987f | Théo Winterhalter | 27 September 2019, 09:33:02 UTC | Merge pull request #307 from MetaCoq/eq-univ-prop Using Prop stuff for eq_universe | 27 September 2019, 09:33:02 UTC |
| 58a0551 | Matthieu Sozeau | 27 September 2019, 09:02:02 UTC | Fix template-coq extraction not extracting the config file | 27 September 2019, 09:02:02 UTC |
