Apply suggestions from code review

math-comp · Dec 12, 2024 · bc8f2b4 · bc8f2b4
1 parent b2dd2aa
commit bc8f2b4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/HB/instance.elpi b/HB/instance.elpi
@@ -43,7 +43,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
   % identify the factory
   std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
   if (factory-alias->gref FactoryAlias Factory) true
-     (coq.error "HB:" {coq.term->string (global FactoryAlias)} "is not a factory or its library was not correctly imported"),
+     (coq.error "HB:" {coq.term->string (global FactoryAlias)} "is not a factory or its library is not correctly imported"),
   std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
 
   % declare the constant for the factory instance

diff --git a/tests/err_bad_mix.v.out b/tests/err_bad_mix.v.out
@@ -2,4 +2,4 @@ Interactive Module Test started
 Interactive Module Exports started
 The command has indeed failed with message:
 HB: Test.Mixin.axioms_ 
-is not a factory or its library was not correctly imported
+is not a factory or its library is not correctly imported