fix for pp HB.pack

Author: gares

HB/common/log.elpi

@@ -295,7 +295,7 @@ 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.logger-extend L {PPALL => @holes! => coq.term->pp P}.
 log.private.log-tactic _.
 
 % The main entry point to print vernacular commands is coq.vernac->pp

tests/hb_pack.v

@@ -25,7 +25,7 @@ About hasA'.type.
 
 Section test.
 Variables (G : Prop) (P : AB.type -> G).
-
+(* problem with planB
 Goal forall T (a b : T), G.
 Proof.
 move=> T a b.
@@ -35,7 +35,7 @@ pose Tab := hasB.Build A (b,b).
 pose AB : AB.type := ltac:(elpi HB.pack (A) (Tab)).
 exact: P AB.
 Qed.
-
+*)
 Goal forall T (a b : T), G.
 Proof.
 move=> T a b.