From 16e8215ccada77cd86fba50fdb408ac0db314a3c Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 15 Jul 2023 09:06:34 +0200 Subject: [PATCH] Revert "Fixing mathcomp after coq/coq#17484" This reverts commit a7986e6d8ecae2405d103ffb7cf92325288b4e63. --- HB/common/log.elpi | 3 --- 1 file changed, 3 deletions(-) diff --git a/HB/common/log.elpi b/HB/common/log.elpi index 2518b0db..0e95e073 100644 --- 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),