| c3703b0 | SimonBoulier | 11 July 2019, 09:45:38 UTC | clean ugraph | 11 July 2019, 09:48:29 UTC |
| d2a6db5 | Théo Winterhalter | 11 July 2019, 09:38:13 UTC | Remove translations | 11 July 2019, 09:38:13 UTC |
| f7267b6 | Théo Winterhalter | 11 July 2019, 09:35:49 UTC | Fix Makefile (?) | 11 July 2019, 09:35:49 UTC |
| 08ad874 | Théo Winterhalter | 11 July 2019, 09:19:13 UTC | Fix AdmittedLemmata Removing proved lemmata | 11 July 2019, 09:19:13 UTC |
| f25cb6c | Théo Winterhalter | 11 July 2019, 08:43:01 UTC | Add PCUICSN and move normalisation in there | 11 July 2019, 09:08:16 UTC |
| b414076 | Théo Winterhalter | 11 July 2019, 08:24:11 UTC | Remove already proven lemma | 11 July 2019, 08:24:11 UTC |
| 631411e | Théo Winterhalter | 11 July 2019, 08:19:36 UTC | Start cleaning SafeChecker and SafeReduce | 11 July 2019, 08:19:36 UTC |
| f99cd28 | Matthieu Sozeau | 11 July 2019, 05:42:58 UTC | Mention the HTML doc in the README for the material | 11 July 2019, 05:42:58 UTC |
| 03a04d0 | Matthieu Sozeau | 11 July 2019, 05:40:03 UTC | Add already built html versions. Update with `make html` at the root. | 11 July 2019, 05:40:03 UTC |
| 2eb6918 | Matthieu Sozeau | 11 July 2019, 05:38:10 UTC | Add a makefile target to produce the "light" documentation | 11 July 2019, 05:38:10 UTC |
| bcfb212 | Matthieu Sozeau | 11 July 2019, 05:17:55 UTC | Clean readme | 11 July 2019, 05:17:55 UTC |
| 2d7eecb | Matthieu Sozeau | 11 July 2019, 05:11:15 UTC | Do not build the (unsafe) extraction plugin | 11 July 2019, 05:11:15 UTC |
| bfc4e21 | Matthieu Sozeau | 11 July 2019, 05:10:50 UTC | Do not build the useless plugins | 11 July 2019, 05:10:50 UTC |
| b95e48c | Matthieu Sozeau | 11 July 2019, 05:09:26 UTC | Remove old checker from this | 11 July 2019, 05:09:26 UTC |
| eed80fe | Matthieu Sozeau | 11 July 2019, 02:24:24 UTC | README for POPL submission material | 11 July 2019, 05:05:26 UTC |
| 32d51e3 | Matthieu Sozeau | 11 July 2019, 02:13:13 UTC | Anonymized archive | 11 July 2019, 04:57:47 UTC |
| 3bc6566 | Yannick Forster | 11 July 2019, 02:07:19 UTC | Fixed compilation (?) | 11 July 2019, 04:35:01 UTC |
| d5eb398 | Yannick Forster | 11 July 2019, 02:05:47 UTC | Added PCUICAdmittedLemmata.v file | 11 July 2019, 04:35:01 UTC |
| 2270475 | Yannick Forster | 11 July 2019, 01:01:05 UTC | update univ subst | 11 July 2019, 04:35:01 UTC |
| 59c35cd | Matthieu Sozeau | 11 July 2019, 04:32:48 UTC | Merge pull request #215 from MetaCoq/safechecker Safechecker - moving modules out of pcuic | 11 July 2019, 04:32:48 UTC |
| 51e217e | Matthieu Sozeau | 10 July 2019, 21:09:41 UTC | Infrastructure for SafeChecker plugin Toplevel configuration Move files, forgot about PCUICPosition, no fixed Actually use a simpler setup without gen-src SafeChecker extraction Fix compilation Fixes in compilation Extraction working, except not! Extraction is buggy Found a pretty deep bug with extraction to OCaml Disable extraction of safechecker, port extraction module Revert "Fixes in compilation" This reverts commit 17ffde1118808e8d3d448abf402d1b329f9b9df6. Revert back to the way extraction was before | 11 July 2019, 04:14:16 UTC |
| 99afafc | Matthieu Sozeau | 10 July 2019, 20:47:32 UTC | Move wellformed_irr to a standard use of proof_irrelevance | 11 July 2019, 04:10:42 UTC |
| dfa9967 | Matthieu Sozeau | 10 July 2019, 20:47:00 UTC | Minor progress in Validity | 11 July 2019, 04:10:42 UTC |
| 45ce8d2 | Théo Winterhalter | 10 July 2019, 22:08:30 UTC | Merge pull request #216 from TheoWinterhalter/cumul-inv Cumulativity inversion for tInd | 10 July 2019, 22:08:30 UTC |
| 011a76b | Théo Winterhalter | 10 July 2019, 21:51:45 UTC | Prove invert_cumul_ind_l | 10 July 2019, 21:51:45 UTC |
| e843af9 | Théo Winterhalter | 10 July 2019, 21:46:38 UTC | Prove invert_red_ind | 10 July 2019, 21:46:38 UTC |
| b541ce6 | Matthieu Sozeau | 10 July 2019, 20:26:46 UTC | Merge pull request #214 from TheoWinterhalter/clean-safeconv Prove mkApps_Prod_nil' | 10 July 2019, 20:26:46 UTC |
| e7a93c7 | Théo Winterhalter | 10 July 2019, 20:23:52 UTC | Prove mkApps_Prod_nil' | 10 July 2019, 20:23:52 UTC |
| 92af0e9 | Matthieu Sozeau | 10 July 2019, 20:23:14 UTC | Merge pull request #213 from TheoWinterhalter/clean-safeconv Prove isAppProd_isProd and maybe more later | 10 July 2019, 20:23:14 UTC |
| 5349685 | Matthieu Sozeau | 10 July 2019, 20:17:48 UTC | Merge pull request #210 from MetaCoq/pcuic-infer-new Cleaning SafeChecker | 10 July 2019, 20:17:48 UTC |
| 540b19c | SimonBoulier | 10 July 2019, 19:51:19 UTC | fix compilation | 10 July 2019, 19:51:19 UTC |
| 16d66cb | SimonBoulier | 10 July 2019, 19:11:25 UTC | WIP | 10 July 2019, 19:20:24 UTC |
| 3022df7 | SimonBoulier | 10 July 2019, 18:35:27 UTC | more on universes and SafeChecker | 10 July 2019, 19:11:35 UTC |
| e66ddc9 | SimonBoulier | 09 July 2019, 07:52:58 UTC | Cleaning in universes | 10 July 2019, 19:11:35 UTC |
| 5c97443 | SimonBoulier | 10 July 2019, 11:25:53 UTC | cleaning SafeChecker | 10 July 2019, 19:11:35 UTC |
| 86e2283 | Théo Winterhalter | 10 July 2019, 18:23:08 UTC | Prove isAppProd_isProd | 10 July 2019, 18:23:08 UTC |
| dca4117 | Théo Winterhalter | 10 July 2019, 17:16:24 UTC | Merge pull request #211 from MetaCoq/red-congr Try to complete congruence of reduction | 10 July 2019, 17:16:24 UTC |
| fbc3389 | Théo Winterhalter | 10 July 2019, 16:50:02 UTC | Merge remote-tracking branch 'origin/coq-8.8' into red-congr | 10 July 2019, 16:50:02 UTC |
| 5e53532 | Théo Winterhalter | 10 July 2019, 16:44:38 UTC | Fix up extraction with respect to red_fix_congr | 10 July 2019, 16:44:38 UTC |
| ec0abf8 | Théo Winterhalter | 10 July 2019, 16:33:56 UTC | Fix uses of red_(co)fix_congr | 10 July 2019, 16:33:56 UTC |
| 7228315 | Théo Winterhalter | 10 July 2019, 15:55:19 UTC | Conclude red_cofix_congr | 10 July 2019, 15:55:19 UTC |
| 1cca89a | Théo Winterhalter | 10 July 2019, 15:48:21 UTC | Prove red_fix_congr | 10 July 2019, 15:48:21 UTC |
| eb43536 | Théo Winterhalter | 10 July 2019, 15:19:09 UTC | Prove red_fix_body | 10 July 2019, 15:19:09 UTC |
| d852e9f | Théo Winterhalter | 10 July 2019, 15:01:56 UTC | Prove red_fix_one_body! | 10 July 2019, 15:01:56 UTC |
| e158bf7 | Théo Winterhalter | 10 July 2019, 14:12:00 UTC | Merge pull request #212 from yforster/new-erasure-2 State of erasure: Move meta-theory stuff to pcuic | 10 July 2019, 14:12:00 UTC |
| 894dd7a | Yannick Forster | 10 July 2019, 13:54:06 UTC | compilation works | 10 July 2019, 13:54:06 UTC |
| 33f44ef | Théo Winterhalter | 10 July 2019, 13:35:32 UTC | Merge pull request #205 from TheoWinterhalter/more-type-rename Proving type_rename more | 10 July 2019, 13:35:32 UTC |
| b94fdbb | Yannick Forster | 10 July 2019, 13:32:40 UTC | Don't require PCUICElimination in Extract.v | 10 July 2019, 13:33:58 UTC |
| 99f3de2 | Yannick Forster | 10 July 2019, 13:19:43 UTC | Move all admitted lemmas needed for erasure to pcuic | 10 July 2019, 13:23:17 UTC |
| 81d1808 | Yannick Forster | 10 July 2019, 12:30:56 UTC | Move stuff on eliminations in own file | 10 July 2019, 13:23:17 UTC |
| 9835d25 | Théo Winterhalter | 10 July 2019, 13:00:22 UTC | Post-merge fix | 10 July 2019, 13:00:22 UTC |
| bfbbde0 | Théo Winterhalter | 10 July 2019, 12:37:47 UTC | The proof is still not clear | 10 July 2019, 12:37:47 UTC |
| ff350da | Théo Winterhalter | 10 July 2019, 12:25:31 UTC | Merge branch 'coq-8.8' into more-type-rename | 10 July 2019, 12:25:31 UTC |
| c5f96ff | Théo Winterhalter | 10 July 2019, 12:21:56 UTC | Reorganise a bit PCUICReduction | 10 July 2019, 12:21:56 UTC |
| 0c083ce | Théo Winterhalter | 10 July 2019, 11:34:57 UTC | Progress on type_rename | 10 July 2019, 11:34:57 UTC |
| e2aa75d | Yannick Forster | 10 July 2019, 10:18:42 UTC | Implement erasure using erasure flags | 10 July 2019, 10:49:46 UTC |
| 315edb6 | Yannick Forster | 10 July 2019, 10:18:24 UTC | Move safe checker to arbitrary params | 10 July 2019, 10:49:46 UTC |
| 4033bfb | Théo Winterhalter | 10 July 2019, 09:21:29 UTC | Move eq_term_it_mkProd_or_LetIn to equality | 10 July 2019, 09:21:29 UTC |
| e777e03 | Théo Winterhalter | 10 July 2019, 09:11:22 UTC | Remove redundant squash notation | 10 July 2019, 09:11:22 UTC |
| 6bc52ba | Théo Winterhalter | 10 July 2019, 09:05:43 UTC | Update type_rename to take in wf Σ | 10 July 2019, 09:05:43 UTC |
| 70f04de | Théo Winterhalter | 10 July 2019, 08:50:00 UTC | Big progress with tCase in type_rename, just missing validity condition | 10 July 2019, 08:50:00 UTC |
| cf5e165 | Théo Winterhalter | 10 July 2019, 08:12:15 UTC | Merge pull request #207 from yforster/new-erasure Another current state of erasure | 10 July 2019, 08:12:15 UTC |
| f92cf6e | Théo Winterhalter | 10 July 2019, 08:11:31 UTC | Prove types_of_case_eq_term | 10 July 2019, 08:11:31 UTC |
| 74835c0 | Théo Winterhalter | 10 July 2019, 08:02:38 UTC | Prove correct version of build_branches_type_eq_term | 10 July 2019, 08:02:38 UTC |
| f217d15 | Théo Winterhalter | 10 July 2019, 07:50:29 UTC | Prove build_branches_type_eq_term, but we need it to be stronger | 10 July 2019, 07:50:29 UTC |
| 63d3e48 | Yannick Forster | 10 July 2019, 07:47:48 UTC | fixed coqproject | 10 July 2019, 07:47:48 UTC |
| 635cf28 | Théo Winterhalter | 10 July 2019, 07:45:01 UTC | Merge pull request #208 from MetaCoq/context_conv Context conv | 10 July 2019, 07:45:01 UTC |
| d351862 | Matthieu Sozeau | 10 July 2019, 06:45:14 UTC | Fix compilation, PCUICSR moved to checker_flags now | 10 July 2019, 06:59:07 UTC |
| 790bafb | Yannick Forster | 10 July 2019, 06:52:39 UTC | Add univ subst file | 10 July 2019, 06:52:39 UTC |
| f895254 | Matthieu Sozeau | 10 July 2019, 06:31:04 UTC | Refactor/Cleanup PCUICSR | 10 July 2019, 06:48:56 UTC |
| feb606e | Matthieu Sozeau | 10 July 2019, 05:20:14 UTC | Renamings, minor refactorings | 10 July 2019, 06:48:56 UTC |
| e2852a6 | Matthieu Sozeau | 10 July 2019, 04:43:07 UTC | Finally proved red1_red_ctx fully! Only congruences remaining (red_fix_congr and the like) | 10 July 2019, 06:48:56 UTC |
| c786b17 | Matthieu Sozeau | 09 July 2019, 20:31:26 UTC | Unsquash theorems in PCUICEquality | 10 July 2019, 06:48:56 UTC |
| a48bcfc | Yannick Forster | 10 July 2019, 00:52:15 UTC | moved typing_univ_subst | 10 July 2019, 00:52:15 UTC |
| 49ea26d | Yannick Forster | 10 July 2019, 00:09:12 UTC | cleanup | 10 July 2019, 00:09:12 UTC |
| d293cb1 | Yannick Forster | 09 July 2019, 23:56:50 UTC | Proved erasure under universe subst! | 09 July 2019, 23:56:50 UTC |
| 40f3c19 | Théo Winterhalter | 09 July 2019, 21:48:45 UTC | Merge pull request #200 from yforster/new-erasure Current progress of erasure | 09 July 2019, 21:48:45 UTC |
| 07248fa | Théo Winterhalter | 09 July 2019, 21:48:16 UTC | Setting a roadmap for the Case case of type_rename | 09 July 2019, 21:48:16 UTC |
| 5d8b473 | Yannick Forster | 09 July 2019, 20:03:46 UTC | Progress | 09 July 2019, 20:03:46 UTC |
| a4b4ffd | Yannick Forster | 09 July 2019, 19:54:45 UTC | Rebased successfully, now there are more admits | 09 July 2019, 19:54:45 UTC |
| 258b34e | Yannick Forster | 09 July 2019, 18:48:37 UTC | two new lines on universes | 09 July 2019, 19:13:36 UTC |
| bf4f740 | Yannick Forster | 09 July 2019, 18:37:09 UTC | EArities.v has only cumul inversions left | 09 July 2019, 19:13:36 UTC |
| a6e8342 | Yannick Forster | 09 July 2019, 16:25:07 UTC | move inversion lemmas to top of EArities.v | 09 July 2019, 19:12:55 UTC |
| 5e5710b | Yannick Forster | 09 July 2019, 11:04:14 UTC | proved subslet_fix_subst | 09 July 2019, 19:12:39 UTC |
| 85ce4a5 | Yannick Forster | 09 July 2019, 00:48:11 UTC | minor progress elim restriction | 09 July 2019, 19:12:01 UTC |
| ed490d0 | Yannick Forster | 09 July 2019, 00:23:30 UTC | Progress | 09 July 2019, 19:12:01 UTC |
| 67a7012 | Yannick Forster | 08 July 2019, 23:37:29 UTC | Several tries on elim restriction and related stuff | 09 July 2019, 19:12:01 UTC |
| 69fccd6 | Yannick Forster | 08 July 2019, 21:27:56 UTC | elim restriction for projections done | 09 July 2019, 19:11:34 UTC |
| 76ae987 | Yannick Forster | 08 July 2019, 21:09:21 UTC | Minor progress, compiles | 09 July 2019, 19:11:34 UTC |
| 881a6f3 | Yannick Forster | 08 July 2019, 19:05:08 UTC | isArity_ind_type and isWfArity_prod_inv | 09 July 2019, 19:10:19 UTC |
| 6d2c96a | Yannick Forster | 08 July 2019, 15:33:57 UTC | Proved closure of isErasable under applications and taking bodies | 09 July 2019, 19:10:19 UTC |
| 8af91ce | Yannick Forster | 08 July 2019, 09:31:52 UTC | Proved termination of is_arity | 09 July 2019, 19:07:21 UTC |
| 250f458 | Yannick Forster | 07 July 2019, 21:28:47 UTC | Finished context conversion for red as needed here | 09 July 2019, 19:06:18 UTC |
| 76e9319 | Yannick Forster | 07 July 2019, 21:16:40 UTC | Worked on context_conversion for red | 09 July 2019, 19:06:18 UTC |
| 3c48e8a | Yannick Forster | 07 July 2019, 18:56:27 UTC | Erasure Function compiles | 09 July 2019, 19:05:34 UTC |
| 5c11150 | Yannick Forster | 07 July 2019, 13:38:18 UTC | make everything compile again | 09 July 2019, 19:04:58 UTC |
| a02a399 | Yannick Forster | 07 July 2019, 13:23:44 UTC | nicer is_erasable function | 09 July 2019, 19:04:58 UTC |
| 7d9f591 | Yannick Forster | 07 July 2019, 13:01:49 UTC | new notation for monads allowing patterns | 09 July 2019, 19:04:58 UTC |
| 6c76a6b | Yannick Forster | 07 July 2019, 12:47:12 UTC | Readable form for erasure functions | 09 July 2019, 19:04:28 UTC |
| e4688ab | Yannick Forster | 07 July 2019, 11:29:45 UTC | Rename is_type_or_proof into is_erasable | 09 July 2019, 19:03:11 UTC |
