logging for hb_instance

HB/common/log.elpi

@@ -196,6 +196,14 @@ log.coq.check Skel Ty T D :- std.do! [
   log.private.log-vernac (log.private.coq.vernac.check Skel Fail),
 ].
 
+pred refine i:term, i:goal, o:list sealed-goal. % to silence a warning, since this is only in tactics
+pred log.refine i:term, i:goal, o:list sealed-goal.
+log.refine T G GL :- std.do! [
+  refine T G GL,
+  G = goal _ _ _ Solution _,
+  log.private.log-tactic Solution,
+].
+
 namespace log.private {
 
 %%%%% Logging Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -241,6 +249,7 @@ type coq.vernac.strategy      list constant -> conversion_strategy -> coq.vernac
 
 pred with-logging i:prop.
 pred log.private.log-vernac i:log.private.coq.vernac.
+pred log.private.log-tactic i:term.
 
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
@@ -276,6 +285,11 @@ log.private.log-vernac V :- log.private.logger L Nice, !,
   log.private.logger-extend L {PPALL => log.private.coq.vernac->pp [V]}.
 log.private.log-vernac _.
 
+log.private.log-tactic P :- log.private.logger L Nice, !,
+  if (Nice = tt) (PPALL = []) (PPALL = [@ppall!]),
+  log.private.logger-extend L {PPALL => coq.term->pp P}.
+log.private.log-tactic _.
+
 % The main entry point to print vernacular commands is coq.vernac->pp
 
 shorten log.private.coq.vernac.{ begin-module , end-module , begin-section, end-section }.

structures.v

@@ -419,7 +419,7 @@ solve (goal _ _ Statement _ Args as G) GLS :- with-attributes (with-logging (std
 
   hb-instance Ty T Factory Instance,
 
-  std.assert! (refine Instance G GLS) "the instance does not solve the goal",
+  std.assert! (log.refine Instance G GLS) "the instance does not solve the goal",
 ])).
 
 }}.