diff --git a/HB/factory.elpi b/HB/factory.elpi
index 690adc4e..33972190 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -96,19 +96,26 @@ kind asset type.
 type asset-mixin asset.
 type asset-factory asset.
 
+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 "HB:" {calc ("The #[key=\"" ^ ID1 ^ "\"] attribute")}
+    "does not match the selected subject" ID.
+
 pred is-key i:indt-decl.
 pred is-key i:arity.
 pred is-key i:context-decl.
-is-key (parameter _ _ _ _\ record _ _ _ _) :- !.
-is-key (parameter _ _ _ _\ inductive _ _ _ _) :- !.
-is-key (parameter _ _ _ _\ arity _) :- !.
-is-key (context-item _ _ _ _ _\ context-end) :- !.
+is-key (parameter ID _ _ _\ record _ _ _ _) :- !, check-key-attribute-consistency ID.
+is-key (parameter ID _ _ _\ inductive _ _ _ _) :- !, check-key-attribute-consistency ID.
+is-key (parameter ID _ _ _\ arity _) :- !, check-key-attribute-consistency ID.
+is-key (context-item ID _ _ _ _\ context-end) :- !, check-key-attribute-consistency ID.
 is-key (parameter ID _ _ _) :- get-option "key" ID, !.
 is-key (context-item ID _ _ _ _) :- get-option "key" ID, !.
-is-key (parameter _ _ _ p\ parameter _ _ (M p) _) :-
-  pi p\ factory? (M p) _, !.
-is-key (context-item _ _ _ _ p\ context-item _ _ (M p) _ _) :-
-  pi p\ factory? (M p) _, !.
+is-key (parameter ID _ _ p\ parameter _ _ (M p) _) :-
+  pi p\ factory? (M p) _, !, check-key-attribute-consistency ID.
+is-key (context-item ID _ _ _ p\ context-item _ _ (M p) _ _) :-
+  pi p\ factory? (M p) _, !, check-key-attribute-consistency ID.
 
 pred mixin-decl-w-mixins i:string, i:string, i:term, i:(term -> A),
   i:(A -> pair (list (w-args mixinname)) A -> prop),
diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local
index b69480aa..1c40a7b1 100644
--- a/Makefile.test-suite.coq.local
+++ b/Makefile.test-suite.coq.local
@@ -21,6 +21,7 @@ post-all::
 	$(call DIFF, tests/compress_coe.v)
 	$(call DIFF, tests/about.v)
 	$(call DIFF, tests/howto.v)
+	$(call DIFF, tests/err_miss_key.v)
 	$(call DIFF, tests/missing_join_error.v)
 	$(call DIFF, tests/not_same_key.v)
 	$(call DIFF, tests/hnf.v)
\ No newline at end of file
diff --git a/tests/err_miss_key.v b/tests/err_miss_key.v
new file mode 100644
index 00000000..491faf03
--- /dev/null
+++ b/tests/err_miss_key.v
@@ -0,0 +1,4 @@
+From HB Require Import structures.
+
+Fail #[key="Tmiss"]
+HB.mixin Record Foo T := {}.
\ No newline at end of file
diff --git a/tests/err_miss_key.v.out b/tests/err_miss_key.v.out
new file mode 100644
index 00000000..8793ae49
--- /dev/null
+++ b/tests/err_miss_key.v.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+HB: The #[key="Tmiss"] attribute does not match the selected subject T