diff --git a/HB/builders.elpi b/HB/builders.elpi
index 56aeec11..3f211a31 100644
--- a/HB/builders.elpi
+++ b/HB/builders.elpi
@@ -31,7 +31,7 @@ begin CtxSkel :-
 % "end" is a keyword, be put it in the namespace by hand
 func builders.end.
 builders.end :- std.do! [
-  current-mode (builder-from _ _ _ ModName),
+  current-mode (builder-from T _ _ ModName),
 
   log.coq.env.end-section-name ModName,
 
@@ -40,8 +40,10 @@ builders.end :- std.do! [
   std.fold LFIL [] builders.private.declare-1-builder Clauses,
 
   if (Clauses = [])
-     (coq.error "No builders to declare, did you forget HB.instance?")
-     true,
+     (coq.error "HB:"
+      { calc ("No builders on " ^ { coq.term->string T } ^ " to declare.") }
+      { calc ("This HB.builders section must HB.instance at least one mixin or factory on " ^ { coq.term->string T } ^ ".") }
+     ) true,
 
   std.findall (abbrev-to-export F_ N_ A_) ExportClauses,
   coq.env.current-path CurModPath,
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 4eaf022a..86b4b843 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -286,12 +286,19 @@ func declare-instance factoryname, term, term
 declare-instance Factory T F Clauses CFL CSL :-
   current-mode (builder-from T TheFactory FGR _), !,
   if (get-option "local" tt)
-    (coq.error "HB: declare-instance: cannot make builders local.
-    If you want temporary instances, make an alias, e.g. with let T' := T") true,
+    (coq.error "HB:" "declare-instance: cannot make builders local."
+      { calc ("If you want temporary instances, make an alias, e.g. with let " ^ { coq.term->string T } ^ "' := " ^ { coq.term->string T } ) }
+    )
+    true,
   !,
   declare-canonical-instances-from-factory-and-local-builders Factory
     T F TheFactory FGR Clauses CFL CSL.
 declare-instance Factory T F Clauses CFL CSL :-
+  if (not (get-option "local" tt),
+      current-mode (builder-from U _ _ _), not (T = U))
+    (coq.warning "HB" "HB.nonlocal-instance-in-builder-mode"
+      "In builder mode, non-builder instances are always considered local.\n"
+      "Annotate this HB.instance call with #[local] to fix this warning and improve your code documentation.") true,
   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
   if (get-option "export" tt)
      (coq.env.current-library File,