bug

math-comp · Oct 1, 2020 · 24fffd3 · 24fffd3
1 parent 95d08e2
commit 24fffd3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/hb.elpi b/hb.elpi
@@ -1787,7 +1787,7 @@ pred postulate-factory-abbrev i:term, i:id, i:factoryname, o:term.
 postulate-factory-abbrev TheType Name Falias TheFactory :- std.do! [
   factory-alias->gref Falias F,
   phant-abbrev F _ Fabv,
-  coq.notation.abbreviation Fabv [TheType] Package,
+  coq.notation.abbreviation Fabv [TheType] Package, % BUG
   Msg is "Unable to declare factory " ^ Name,
   std.assert-ok! (coq.typecheck-ty Package _) Msg,
   @local! => hb-add-const Name _ Package @opaque! C,