HB.instance: improve error message when declaring local builder

Author: lweqx

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.