Apply suggestions from code review

math-comp · Dec 12, 2024 · 7d8cf23 · 7d8cf23
1 parent a5f9712
commit 7d8cf23
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/HB/factory.elpi b/HB/factory.elpi
@@ -100,7 +100,7 @@ pred check-key-attribute-consistency i:id.
 check-key-attribute-consistency _ :- not(get-option "key" _), !.
 check-key-attribute-consistency ID :- get-option "key" ID, !.
 check-key-attribute-consistency ID :- get-option "key" ID1,
-  coq.error {calc ("The #[key=\"" ^ ID1 ^ "\"] attribute")}
+  coq.error "HB:" {calc ("The #[key=\"" ^ ID1 ^ "\"] attribute")}
     "does not match the selected subject" ID.
 
 pred is-key i:indt-decl.

diff --git a/tests/err_miss_key.v.out b/tests/err_miss_key.v.out
@@ -1,2 +1,2 @@
 The command has indeed failed with message:
-The #[key="Tmiss"] attribute does not match the selected subject T
+HB: The #[key="Tmiss"] attribute does not match the selected subject T