| d76226c | Abhishek Anand (optiplex7010@home) | 25 October 2019, 16:07:27 UTC | some work on automatic translation from TemplateMonad to TM | 25 October 2019, 16:07:27 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 |
| 1292d49 | Matthieu Sozeau | 27 September 2019, 08:11:11 UTC | Merge pull request #303 from MetaCoq/opam-translations Make opam package for translations as well | 27 September 2019, 08:11:11 UTC |
| 333d010 | Théo Winterhalter | 26 September 2019, 15:55:24 UTC | Using Prop stuff for eq_universe | 26 September 2019, 18:10:53 UTC |
| 6a3c570 | Gregory Malecha | 26 September 2019, 16:18:52 UTC | support for opaque definitions in the core monad. | 26 September 2019, 16:45:53 UTC |
| 6240983 | Gregory Malecha | 26 September 2019, 14:23:17 UTC | support for opaque definitions - only in the extractable monad. | 26 September 2019, 16:45:53 UTC |
| 5be172b | Matthieu Sozeau | 26 September 2019, 14:39:32 UTC | Fix import | 26 September 2019, 14:39:32 UTC |
| 1ee18a7 | Matthieu Sozeau | 26 September 2019, 13:39:49 UTC | Fix configuration of translations package | 26 September 2019, 14:09:33 UTC |
| bf1e86f | Théo Winterhalter | 26 September 2019, 14:06:40 UTC | Merge pull request #302 from MetaCoq/conv-args More symmetric approach to conversion of stacks | 26 September 2019, 14:06:40 UTC |
| eaa0ec0 | Théo Winterhalter | 26 September 2019, 13:34:58 UTC | Use leq in the leq branch of fallback | 26 September 2019, 13:34:58 UTC |
| 5c5f93f | Matthieu Sozeau | 26 September 2019, 13:16:05 UTC | Add translations to the global package | 26 September 2019, 13:16:05 UTC |
| b43ed8c | Matthieu Sozeau | 26 September 2019, 13:01:24 UTC | Make opam package for translations as well | 26 September 2019, 13:01:24 UTC |
| e6782a1 | Matthieu Sozeau | 26 September 2019, 12:40:40 UTC | Update .gitignore | 26 September 2019, 12:41:05 UTC |
| 243abdd | SimonBoulier | 26 September 2019, 11:20:41 UTC | Making translations compiling again | 26 September 2019, 12:10:08 UTC |
| 54a4fe2 | Matthieu Sozeau | 26 September 2019, 12:08:55 UTC | Merge pull request #299 from yforster/Ecbveval_fixes Prove admits in evaluation relation for erased terms | 26 September 2019, 12:08:55 UTC |
| 45acabd | Théo Winterhalter | 25 September 2019, 15:33:51 UTC | Give isconv_args two terms instead of one to account for cumul Removes need for `wellformed_zipc_replace`! | 26 September 2019, 11:21:55 UTC |
| 69296b4 | Yannick Forster | 26 September 2019, 10:35:49 UTC | fix compilation | 26 September 2019, 10:35:49 UTC |
| ec2d4a3 | Théo Winterhalter | 25 September 2019, 15:25:38 UTC | Merge pull request #297 from MetaCoq/lexmod Conversion well-order modulo universes | 25 September 2019, 15:25:38 UTC |
| 291e7ac | Théo Winterhalter | 25 September 2019, 15:01:13 UTC | Admit wellformed_eq_term to close remaining obligations | 25 September 2019, 15:01:13 UTC |
| 780bb64 | Théo Winterhalter | 25 September 2019, 14:39:20 UTC | Replace eq_dec with eqb_universe_instance | 25 September 2019, 14:39:20 UTC |
| ea6c3bf | Théo Winterhalter | 25 September 2019, 12:13:33 UTC | Use new order for safe conversion | 25 September 2019, 13:41:48 UTC |
| e198d26 | Yannick Forster | 25 September 2019, 08:30:33 UTC | prove value_app_inv | 25 September 2019, 08:37:18 UTC |
| 74bcc82 | Yannick Forster | 24 September 2019, 13:27:35 UTC | Close admits in extracted cbv evaluation | 25 September 2019, 08:37:18 UTC |
| f1fe111 | Matthieu Sozeau | 24 September 2019, 23:10:57 UTC | Merge pull request #298 from MetaCoq/vscode-config Add VSCode config | 24 September 2019, 23:10:57 UTC |
| 02841b0 | Matthieu Sozeau | 24 September 2019, 23:00:16 UTC | Fix Equations version for testing | 24 September 2019, 23:00:16 UTC |
| 2243d1f | Matthieu Sozeau | 24 September 2019, 22:29:07 UTC | Update .travis.yml to fix travis "unauthenticated package" error | 24 September 2019, 22:29:07 UTC |
