Merge pull request math-comp#372 from proux01/coq_17484

Fixing mathcomp after coq/coq#17484
proux01 · Jul 6, 2023 · 85fab30 · 85fab30
2 parents c8e542e + a7986e6
commit 85fab30
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/HB/common/log.elpi b/HB/common/log.elpi
@@ -35,6 +35,7 @@ env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
+  coq.typecheck Bo Ty _,
   coq.env.add-const Name1 Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
@@ -49,6 +50,7 @@ env.add-const Name Bo Ty Opaque C :- std.do! [
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
+  coq.typecheck Bo Ty _,
   coq.env.add-const Name1 Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
@@ -61,6 +63,7 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [
     (coq.error "HB: cannot infer some information in" Name
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
+  coq.typecheck Bo Ty _,
   coq.env.add-const Name Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),