issues
search
MetaCoq
/
metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
368
stars
79
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Adapt to https://github.com/coq/coq/pull/19530
#1102
proux01
opened
3 days ago
0
Take relevance into account for typing
#1101
yannl35133
opened
4 days ago
0
Bump cachix/install-nix-action from V27 to 28
#1100
dependabot[bot]
closed
4 days ago
0
Add PCUICESubst file to verify Coq code
#1099
yannl35133
opened
2 weeks ago
0
Typecheck the result of term unquotation.
#1098
ppedrot
closed
3 weeks ago
4
Add Nix flakes-based build scripts
#1097
spacefrogg
opened
1 month ago
2
Adapt to coq/coq#19384 (add_global_univ -> add_forgotten_univ)
#1096
SkySkimmer
closed
1 month ago
0
Proof that reordering of constructors is correct
#1095
mattam82
closed
2 months ago
0
Point 'index' in CoqDocJS header to index.html
#1094
SwampertX
closed
4 days ago
1
Adapt to https://github.com/coq/coq/pull/19310
#1093
proux01
closed
1 week ago
2
Remove generated files from archive and ignore them now
#1092
mattam82
closed
2 months ago
0
`Unquote Definition` will normalize the term
#1091
WeituoDAI
opened
2 months ago
0
Universe inconsistency with MetaCoq and stdpp
#1090
4ever2
closed
2 weeks ago
4
Add the `force (lazy t)` evaluation rule to LambdaBox
#1089
mattam82
closed
3 months ago
0
Adapt to coq/coq#18973.
#1088
rlepigre
closed
3 months ago
5
Correcting the definition of noccur_between in Template – main branch
#1087
MevenBertrand
closed
4 days ago
0
Correct noccur for Template
#1086
MevenBertrand
closed
4 days ago
0
Fixes for funelim
#1085
mattam82
closed
4 months ago
0
Bump cachix/cachix-action from 14 to 15
#1084
dependabot[bot]
closed
4 months ago
0
Adapt to Coq PR #18795 (more uniform API for declare.ml)
#1083
herbelin
closed
3 months ago
0
Bump cachix/install-nix-action from 25 to 27
#1082
dependabot[bot]
closed
4 months ago
0
faster PCUICSR
#1081
mrhaandi
closed
3 months ago
6
Adapt to coq/coq#18938 (EConstr.ERelevance)
#1080
SkySkimmer
closed
5 months ago
0
Remove useless calls to Eval vm_compute.
#1079
silene
closed
3 months ago
0
Adapt to coq PR #18921 fixing bugs of the inference of the return clause for Program-style pattern-matching
#1078
herbelin
closed
5 months ago
0
Adapt w.r.t. coq/coq#18909.
#1077
ppedrot
closed
5 months ago
0
Adapt w.r.t. coq/coq#18910.
#1076
ppedrot
closed
5 months ago
0
Take relevance into account for typing
#1075
yannl35133
closed
4 days ago
1
Adapt to coq/coq#18422 (indirect accessor handled through vernactypes)
#1074
SkySkimmer
closed
5 months ago
1
Adapt to coq/coq#18867 (inductive_sort_family doesn't exist)
#1073
SkySkimmer
closed
5 months ago
0
Anomaly as a result of extraction in CertiCoq (assertion fails in ml code)
#1072
mkarup
opened
5 months ago
3
Adapt to coq/coq#18852 (interp_red_expr can be done without ltac)
#1071
SkySkimmer
closed
5 months ago
0
Fix the translation of cofix to fix
#1070
mattam82
closed
5 months ago
4
Please create a tag for Coq 8.19 in Coq Platform 2024.01
#1069
rtetley
closed
6 months ago
3
Fix issue #1042 MetaCoq Run does not support evars.
#1068
mattam82
closed
6 months ago
0
Bump cachix/install-nix-action from 25 to 26
#1067
dependabot[bot]
closed
4 months ago
1
Fix inlining and reorder constructors which were not translating let …
#1066
mattam82
closed
6 months ago
0
Fix typo
#1065
mattam82
closed
6 months ago
0
Unsafe and ewcbvevalnamed
#1064
mattam82
closed
6 months ago
0
Implement a general Show typeclass in MetaCoq.Utils
#1063
mattam82
closed
6 months ago
4
Please create a tag for the version of MetaCoq that CertiCoq can depend on
#1062
liyishuai
closed
6 months ago
1
Unsafe inline beta and unboxing transforms
#1061
mattam82
closed
6 months ago
0
Adapt to coq/coq#18038 (rewrite rules)
#1060
yannl35133
closed
7 months ago
0
Reorder constructors
#1059
mattam82
closed
7 months ago
0
Implement tLazy and tForce in EAst
#1058
mattam82
closed
7 months ago
0
Avoid Ee := EWcbvEval module aliases which result in ugly extraction …
#1057
mattam82
closed
7 months ago
0
Resurrect the cofix transform, adding a new axiom for the admitted pr…
#1056
mattam82
closed
7 months ago
0
Adapt to https://github.com/coq/coq/pull/18590
#1055
proux01
closed
7 months ago
1
generalize verified_erasure_pipeline_lookup_env_in
#1054
tabareau
closed
7 months ago
0
Erase function lemma
#1053
mattam82
closed
7 months ago
0
Next