Revert "Fixing mathcomp after coq/coq#17484"

This reverts commit a7986e6.
proux01 · Jul 15, 2023 · 16e8215 · 16e8215
1 parent 85fab30
commit 16e8215
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/HB/common/log.elpi b/HB/common/log.elpi
@@ -35,7 +35,6 @@ 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),
@@ -50,7 +49,6 @@ 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),
@@ -63,7 +61,6 @@ 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),