5e95cc0 | Matthieu Sozeau | 27 September 2019, 16:26:10 UTC | Add extraction with time bounds reference in the Papers section | 27 September 2019, 16:32:01 UTC |
1857541 | 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:02:04 UTC |
5d23584 | Matthieu Sozeau | 27 September 2019, 15:39:42 UTC | Remove useless and misleading "version" field from local opam files | 27 September 2019, 15:39:42 UTC |
ad579b6 | Matthieu Sozeau | 27 September 2019, 14:50:29 UTC | Rework README.md | 27 September 2019, 15:38:12 UTC |
78a8549 | Matthieu Sozeau | 27 September 2019, 14:34:35 UTC | Fix README.md | 27 September 2019, 15:35:19 UTC |
a5650e1 | Matthieu Sozeau | 27 September 2019, 13:47:47 UTC | Fix local config for building translations and README.md | 27 September 2019, 13:54:59 UTC |
2c20267 | Matthieu Sozeau | 27 September 2019, 13:20:26 UTC | Fixes in README.md | 27 September 2019, 13:27:38 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 |
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 |
5df6a23 | Matthieu Sozeau | 24 September 2019, 20:53:39 UTC | Add VSCode config | 24 September 2019, 20:53:39 UTC |
9978626 | Matthieu Sozeau | 24 September 2019, 20:31:20 UTC | Fix #238 : PCUICWcbvEval missing tInd case | 24 September 2019, 20:31:20 UTC |
203c0d4 | Matthieu Sozeau | 24 September 2019, 19:00:17 UTC | Updated README.md | 24 September 2019, 19:00:42 UTC |
f800036 | Matthieu Sozeau | 23 September 2019, 12:24:16 UTC | Update .gitignore | 24 September 2019, 19:00:42 UTC |
7ad4070 | Théo Winterhalter | 24 September 2019, 16:01:42 UTC | Complete R_aux'_Acc proof | 24 September 2019, 16:01:42 UTC |
4e6659f | Théo Winterhalter | 24 September 2019, 14:51:10 UTC | Complete new R_aux definition, partial Acc proof | 24 September 2019, 14:51:10 UTC |
77b5f8a | Théo Winterhalter | 24 September 2019, 12:50:55 UTC | Begin proving R_aux'_Acc | 24 September 2019, 12:50:55 UTC |
3af1d53 | Théo Winterhalter | 24 September 2019, 12:19:30 UTC | Prove dlexmod_Acc | 24 September 2019, 12:19:30 UTC |
21defbe | Théo Winterhalter | 24 September 2019, 12:00:10 UTC | Tweak notation to define R_aux alternatively | 24 September 2019, 12:00:10 UTC |
d7b31c7 | Théo Winterhalter | 24 September 2019, 11:43:33 UTC | Define eq_term_pos | 24 September 2019, 11:43:33 UTC |
4d1488b | Théo Winterhalter | 24 September 2019, 10:01:36 UTC | Prove eq_term_valid_pos | 24 September 2019, 10:01:36 UTC |
ec89883 | Théo Winterhalter | 24 September 2019, 09:36:49 UTC | Make cored' modulo eq_term instead of upto_names | 24 September 2019, 09:40:05 UTC |
0bf890f | Théo Winterhalter | 24 September 2019, 08:10:21 UTC | Comment on how to proceed | 24 September 2019, 08:32:27 UTC |
ac0ee5d | Théo Winterhalter | 23 September 2019, 13:01:38 UTC | Complete acc_dlexmod | 23 September 2019, 13:01:38 UTC |
9c9f9f1 | Théo Winterhalter | 23 September 2019, 12:30:32 UTC | Introduce sym/trans for coe in dlexmod | 23 September 2019, 12:30:32 UTC |
82f33ab | Théo Winterhalter | 23 September 2019, 12:01:12 UTC | Finding more about requirements of acc_dlexmod | 23 September 2019, 12:01:12 UTC |
e1cd1b5 | Théo Winterhalter | 23 September 2019, 08:14:38 UTC | Deal with first case of acc_dlexmod | 23 September 2019, 08:14:38 UTC |
2800d3c | Théo Winterhalter | 22 September 2019, 20:01:01 UTC | Some remarks on how to proceed | 22 September 2019, 20:01:01 UTC |
502050c | Théo Winterhalter | 22 September 2019, 18:07:12 UTC | Begin defining depdent lexicographic order modulo | 22 September 2019, 18:07:12 UTC |
e85f9e7 | Matthieu Sozeau | 21 September 2019, 08:19:01 UTC | Merge pull request #296 from MetaCoq/backport-from-clean Backport from clean | 21 September 2019, 08:19:01 UTC |
6b47227 | Matthieu Sozeau | 20 September 2019, 10:59:59 UTC | Fixed html target, re-add Local Set Keyed Unif | 20 September 2019, 11:44:14 UTC |
3a8ffd1 | Matthieu Sozeau | 20 September 2019, 11:15:15 UTC | Remove obsolete file | 20 September 2019, 11:44:14 UTC |
f3850da | Matthieu Sozeau | 20 September 2019, 11:08:32 UTC | Merge pull request #271 from yforster/remove_case_optimisations Remove case optimisations and fix regressions in erasure | 20 September 2019, 11:08:32 UTC |
ffc322b | Matthieu Sozeau | 20 September 2019, 10:10:56 UTC | Merge branch 'coq-8.8' into remove_case_optimisations | 20 September 2019, 10:10:56 UTC |
a710009 | Matthieu Sozeau | 20 September 2019, 09:56:57 UTC | Merge pull request #294 from MetaCoq/erase-timing Erase timing | 20 September 2019, 09:56:57 UTC |
c8fc338 | Yannick Forster | 20 September 2019, 09:33:04 UTC | no admits | 20 September 2019, 09:33:04 UTC |
28bbbb7 | Matthieu Sozeau | 20 September 2019, 08:53:48 UTC | Fix Makefile dependencies for test-suite, add vs example from CertiCoq | 20 September 2019, 09:32:31 UTC |
32bdca8 | Yannick Forster | 20 September 2019, 09:27:17 UTC | this version is provable | 20 September 2019, 09:27:17 UTC |
efca71f | Yannick Forster | 20 September 2019, 09:17:19 UTC | fixed compilation | 20 September 2019, 09:17:19 UTC |
70c6b54 | Yannick Forster | 20 September 2019, 09:02:42 UTC | Merge remote-tracking branch 'origin/coq-8.8' into remove_case_optimisations | 20 September 2019, 09:02:42 UTC |
af1e517 | Yannick Forster | 20 September 2019, 08:55:23 UTC | One lemma missing, then erasure is finished again | 20 September 2019, 08:55:23 UTC |
50c707b | Matthieu Sozeau | 20 September 2019, 08:35:50 UTC | Timing info in MetaCoq Erase as well and add safechecker_test and erasure_test to the test-suite build | 20 September 2019, 08:41:33 UTC |
f4cbdf3 | Matthieu Sozeau | 20 September 2019, 08:27:43 UTC | Timing info in MetaCoq CoqCheck and SafeCheck | 20 September 2019, 08:27:59 UTC |
e6c70ee | Matthieu Sozeau | 20 September 2019, 08:27:23 UTC | Merge pull request #286 from MetaCoq/unsafe-checker Unsafe checker | 20 September 2019, 08:27:23 UTC |
4ab5ec0 | Yannick Forster | 20 September 2019, 07:38:17 UTC | Fix all universe issues | 20 September 2019, 07:38:17 UTC |
1ae81f0 | Matthieu Sozeau | 20 September 2019, 07:28:29 UTC | Remove ast_id_quoter | 20 September 2019, 07:28:29 UTC |
138523e | Théo Winterhalter | 18 September 2019, 14:37:55 UTC | Unsafe checker command running. We don't get inductive dependencies yet. | 20 September 2019, 07:18:18 UTC |
5aa4b46 | Théo Winterhalter | 19 September 2019, 10:18:10 UTC | Add HoTT test for checker | 20 September 2019, 07:17:52 UTC |
180899d | Théo Winterhalter | 19 September 2019, 10:17:59 UTC | Dummy version of unsafe checker | 20 September 2019, 07:16:55 UTC |
27ae1a6 | Théo Winterhalter | 18 September 2019, 14:37:55 UTC | WIP unsafe checker command | 20 September 2019, 07:16:55 UTC |
8cd855e | Matthieu Sozeau | 20 September 2019, 07:08:49 UTC | Merge pull request #292 from MetaCoq/fix-opam-install Fix opam install | 20 September 2019, 07:08:49 UTC |
da32cdb | Yannick Forster | 20 September 2019, 06:48:14 UTC | fix compilation | 20 September 2019, 06:48:14 UTC |
d69b84f | Matthieu Sozeau | 19 September 2019, 22:27:54 UTC | Update travis config and toplevel Makefile to test opam install | 20 September 2019, 06:41:32 UTC |
53f9703 | Yannick Forster | 20 September 2019, 06:32:24 UTC | Merge remote-tracking branch 'origin/univ_subst_wk' into remove_case_optimisations | 20 September 2019, 06:32:24 UTC |
87a6baf | Théo Winterhalter | 19 September 2019, 22:58:37 UTC | Merge pull request #291 from MetaCoq/conversion-unfold Unfold constants more in safe conversion | 19 September 2019, 22:58:37 UTC |
e26ae65 | Matthieu Sozeau | 19 September 2019, 22:09:40 UTC | Qualify Template/Checker imports more precisely | 19 September 2019, 22:09:40 UTC |
758f11a | Théo Winterhalter | 19 September 2019, 21:36:39 UTC | Unfold constants more in safe conversion | 19 September 2019, 21:40:37 UTC |
c502a6a | Théo Winterhalter | 19 September 2019, 21:18:44 UTC | Merge pull request #290 from MetaCoq/conversion-fix Change checker printing a bit for clarity | 19 September 2019, 21:18:44 UTC |
8069f04 | Théo Winterhalter | 19 September 2019, 20:55:46 UTC | Readd parentheses around rhs of application | 19 September 2019, 20:55:46 UTC |
1f19520 | Théo Winterhalter | 19 September 2019, 20:28:45 UTC | Change checker printing a bit for clarity | 19 September 2019, 20:46:31 UTC |
69ca2aa | Théo Winterhalter | 19 September 2019, 20:39:20 UTC | Merge pull request #288 from MetaCoq/conversion-fix Add missing case on conversion fallback | 19 September 2019, 20:39:20 UTC |
d972f5c | Théo Winterhalter | 19 September 2019, 20:13:56 UTC | Add one more fallback just in case | 19 September 2019, 20:13:56 UTC |
238c7d7 | Théo Winterhalter | 19 September 2019, 20:02:49 UTC | Fix conversion after putting context conversion as hyp | 19 September 2019, 20:02:49 UTC |
0d41cf6 | Théo Winterhalter | 19 September 2019, 18:12:22 UTC | [WIP] Require conv_ctx_stack instead of proving it | 19 September 2019, 18:12:22 UTC |
4c53d82 | Théo Winterhalter | 19 September 2019, 16:32:28 UTC | Dealing with incompleteness a bit | 19 September 2019, 16:32:28 UTC |
a3c47d0 | Matthieu Sozeau | 19 September 2019, 15:44:15 UTC | Merge pull request #284 from yforster/configure-for-opam Add configure.sh to opam files | 19 September 2019, 15:44:15 UTC |
34acd83 | Théo Winterhalter | 19 September 2019, 15:09:37 UTC | Only compare stacks with Conv and not Cumul, using nleq_term first | 19 September 2019, 15:09:37 UTC |
e74add0 | Matthieu Sozeau | 19 September 2019, 10:38:28 UTC | Fix compile time dependencies of plugins in global and local installation mode | 19 September 2019, 14:54:47 UTC |
f33d84a | SimonBoulier | 19 September 2019, 13:11:05 UTC | Weaken the assumptions in UnivSubst lemmas | 19 September 2019, 14:17:53 UTC |
f54fa89 | Yannick Forster | 19 September 2019, 14:11:01 UTC | fix erasure test-suite for now | 19 September 2019, 14:11:01 UTC |
7e8f9ec | Théo Winterhalter | 19 September 2019, 14:10:35 UTC | Add missing case on conversion fallback There is a slight problem with the obligations that are generated though... | 19 September 2019, 14:10:35 UTC |
23da953 | Yannick Forster | 19 September 2019, 14:06:35 UTC | Finished fix unfolding | 19 September 2019, 14:06:35 UTC |
30ca9f4 | SimonBoulier | 19 September 2019, 13:11:05 UTC | Weaken the assumptions in UnivSubst lemmas | 19 September 2019, 13:11:05 UTC |
6cd59a2 | Yannick Forster | 19 September 2019, 10:43:20 UTC | add partial decider for irreducibility | 19 September 2019, 10:43:20 UTC |
b24e072 | Matthieu Sozeau | 19 September 2019, 10:14:00 UTC | Apply Extraction -> erasure renaming everywhere | 19 September 2019, 10:19:31 UTC |
94cd659 | SimonBoulier | 19 September 2019, 09:39:43 UTC | leb kelim instead of eq for type_Case | 19 September 2019, 10:11:38 UTC |
cd693e6 | Matthieu Sozeau | 19 September 2019, 09:34:09 UTC | Separate compilation fixes | 19 September 2019, 10:09:23 UTC |
1ae0d4a | Yannick Forster | 19 September 2019, 10:04:26 UTC | app cong case closed | 19 September 2019, 10:04:26 UTC |