diff --git a/hb.elpi b/hb.elpi index 4a638b90..c8f51bd2 100644 --- 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,