From 9d88e5c93dcae733555a6b22c2ffd93d3edaa7e1 Mon Sep 17 00:00:00 2001
From: Lucie <135951230+lweqx@users.noreply.github.com>
Date: Thu, 16 Oct 2025 15:34:05 +0200
Subject: [PATCH 1/3] HB.instance: warn on nonlocal declaration in builder mode

---
 HB/instance.elpi | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/HB/instance.elpi b/HB/instance.elpi
index 4eaf022a..8179aec4 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -292,6 +292,11 @@ declare-instance Factory T F Clauses CFL CSL :-
   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,

From 85368b451f64a019aaeca0bf110bb5019833819b Mon Sep 17 00:00:00 2001
From: Lucie <135951230+lweqx@users.noreply.github.com>
Date: Thu, 16 Oct 2025 15:34:47 +0200
Subject: [PATCH 2/3] HB.end: improve error message when no builders are
 declared

---
 HB/builders.elpi | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

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,

From a435ffeb01ec6add5533b94163304ba90bf3d994 Mon Sep 17 00:00:00 2001
From: Lucie <135951230+lweqx@users.noreply.github.com>
Date: Thu, 16 Oct 2025 15:34:55 +0200
Subject: [PATCH 3/3] HB.instance: improve error message when declaring local
 builder

---
 HB/instance.elpi | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/HB/instance.elpi b/HB/instance.elpi
index 8179aec4..86b4b843 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -286,8 +286,10 @@ 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.