We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b24b884 commit cd83f0aCopy full SHA for cd83f0a
.gitignore
@@ -413,3 +413,4 @@ template-rocq/_TemplateRocqProject
413
.gitignore
414
template-rocq/_PluginProject
415
template-rocq/_RocqProject
416
+template-rocq/Makefile.template.conf
erasure/theories/ERemapInductives.v
@@ -65,7 +65,7 @@ Section Remap.
65
match lookup_inductive_assoc mapping (fst i) with
66
| None => tCase i c brs
67
| Some tr =>
68
- mkApps (tConst tr.(elim)) (map make_branch brs)
+ mkApps (tConst tr.(elim)) (c :: map make_branch brs)
69
end.
70
71
Equations remap (t : term) : term :=
template-rocq/Makefile.template.conf
0 commit comments