| eff8fe1 | 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:28:38 UTC |
| 914e4c6 | Matthieu Sozeau | 16 November 2019, 13:22:14 UTC | Also mention Théo's README.md files in pcuic/ and safechecker/ | 16 November 2019, 13:22:14 UTC |
| 80a472d | nicolas tabareau | 12 November 2019, 17:11:55 UTC | fix dependency to coq-equation version 1.2 | 12 November 2019, 17:11:55 UTC |
| 23c3832 | Matthieu Sozeau | 12 November 2019, 14:12:03 UTC | Fixes in short installation instructions | 12 November 2019, 14:12:03 UTC |
| 0fb1951 | Matthieu Sozeau | 22 October 2019, 11:58:53 UTC | Fix typos | 22 October 2019, 11:58:53 UTC |
| b7e50b2 | Matthieu Sozeau | 22 October 2019, 11:52:49 UTC | Add correspondence table paper/code | 22 October 2019, 11:54:28 UTC |
| ecfa45c | Matthieu Sozeau | 22 October 2019, 11:31:06 UTC | Fix metacoq_safechecker wrong timing | 22 October 2019, 11:31:06 UTC |
| eafc67e | Matthieu Sozeau | 22 October 2019, 10:34:54 UTC | Update README.md with artifact information at top and add html files | 22 October 2019, 10:56:10 UTC |
| f4d92d5 | Théo Winterhalter | 22 October 2019, 09:46:10 UTC | Merge pull request #322 from yforster/popl-artifact-eval Popl artifact eval erasure | 22 October 2019, 09:46:10 UTC |
| 95bc333 | Yannick Forster | 22 October 2019, 09:20:31 UTC | take in safe erasure again | 22 October 2019, 09:20:31 UTC |
| c5ca2b3 | Yannick Forster | 21 October 2019, 20:46:14 UTC | don't compile the safe erasure functions, it's just an optimisation | 21 October 2019, 20:46:14 UTC |
| 3ccc897 | Yannick Forster | 21 October 2019, 20:18:10 UTC | Merge pull request #7 from yforster/personal/popl-artifact-eval Personal/popl artifact eval | 21 October 2019, 20:18:10 UTC |
| 379d9f0 | Yannick Forster | 21 October 2019, 20:14:37 UTC | Merge remote-tracking branch 'origin/coq-8.9' into personal/popl-artifact-eval | 21 October 2019, 20:14:37 UTC |
| eb8894e | Yannick Forster | 21 October 2019, 20:08:16 UTC | Add full printing | 21 October 2019, 20:08:16 UTC |
| 266f4fc | Yannick Forster | 21 October 2019, 20:01:58 UTC | Merge branch 'popl-artifact-eval' of https://github.com/MetaCoq/metacoq into popl-artifact-eval | 21 October 2019, 20:01:58 UTC |
| cdacc4d | Yannick Forster | 21 October 2019, 20:01:36 UTC | state elim restriction | 21 October 2019, 20:01:36 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 |
| 791861c | nicolas tabareau | 21 October 2019, 15:23:37 UTC | clean safechecker_test.v | 21 October 2019, 15:23:37 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 |
| b64baba | Théo Winterhalter | 21 October 2019, 13:11:05 UTC | Clean admits in PCUIC | 21 October 2019, 13:20:03 UTC |
| cc912ac | Théo Winterhalter | 21 October 2019, 12:19:17 UTC | Remove admits in safechecker | 21 October 2019, 12:19:17 UTC |
| 275e2fd | Théo Winterhalter | 21 October 2019, 11:34:15 UTC | Truly remove Construct_Ind_ind_eq axiom | 21 October 2019, 11:44:02 UTC |
| df40995 | Théo Winterhalter | 21 October 2019, 11:06:34 UTC | Remove Construct_Ind_ind_eq axiom This implies making the checker check for more things. | 21 October 2019, 11:14:37 UTC |
| 3a5d0ec | Théo Winterhalter | 21 October 2019, 09:29:25 UTC | Remove axiom Proj_red_cond Reduction just has an inaccessible branch now. | 21 October 2019, 09:29:25 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 |
