Skip to main content

Browse the archive

https://github.com/MevenBertrand/metacoq
07 June 2021, 07:55:30 UTC
sort by:
Revision Author Date Message Commit Date
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
back to top