From 9c3d854da9fde4702edb3a78827fa3042da4f834 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 27 Aug 2022 15:28:52 +0200
Subject: [PATCH 1/4] fix loc printing

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

diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index 2c3be8db9..01979cfb5 100644
--- a/HB/common/log.elpi
+++ b/HB/common/log.elpi
@@ -266,8 +266,8 @@ pred log.private.log-tactic i:term.
 
 with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.log.raw" _, NICE = ff), !,
   get-option "elpi.loc" Loc,
-  loc.fields Loc FILE _ _ _ _,
-  std.any->string Loc LocStr,
+  loc.fields Loc FILE Start Stop _ _,
+  LocStr is "characters " ^ {std.any->string Start} ^ "-" ^ {std.any->string Stop},
   FILENAME is FILE ^ ".hb",
   open_append FILENAME OC1,
   std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",LocStr,""] PATCH1,

From 78ba9b6da3f6e6bf7d6ad22788aa7843d7035925 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 27 Aug 2022 16:49:33 +0200
Subject: [PATCH 2/4] fix param printing

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

diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index 01979cfb5..a6e28ee96 100644
--- a/HB/common/log.elpi
+++ b/HB/common/log.elpi
@@ -446,8 +446,8 @@ coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :-
 pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp.
 coq.vernac->ppinductiveparams [] [].
 coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :-
-  PP = [box (hov 2) [str A,str ID,str " : ", TY,str B]|PPRest],
-  decl T Name Ty, coq.name->id Name ID, coq.term->pp Ty TY,
+  PP = [box (hov 2) [str A,ID,str " : ", TY,str B]|PPRest],
+  coq.term->pp T ID, decl T _ Ty, coq.term->pp Ty TY,
   if2 (Imp = explicit) (A = "(", B = ")")
       (Imp = maximal)  (A = "{", B = "}")
                        (A = "[", B = "]"),

From 22688a31a1aaa4c777aee0a0b3b31bc58b374871 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 27 Aug 2022 17:26:54 +0200
Subject: [PATCH 3/4] quick fix for reversible coercions

---
 HB/common/log.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index a6e28ee96..6141af0c5 100644
--- a/HB/common/log.elpi
+++ b/HB/common/log.elpi
@@ -361,7 +361,7 @@ coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notati
   coq.vernac->ppabbrterm NParams Term StrParams B.
 coq.vernac->pp1 (canonical Name Local) (box h [Locality, str "Canonical ", str Name, str "."]) :-
   local->locality Local Locality.
-coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :-
+coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "#[reversible] Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :-
   coq.gref->path SRC SP, std.string.concat "." {std.take-last 2 SP} S', S is S' ^ "." ^ {coq.gref->id SRC},
   if2 (TGT = sortclass) (T = "Sortclass")
       (TGT = funclass)  (T = "Funclass")

From edd65165d8cebb15db5d1fa3dfe140342e3a14d2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 27 Aug 2022 22:08:38 +0200
Subject: [PATCH 4/4] fix for pp HB.pack

---
 HB/common/log.elpi | 2 +-
 tests/hb_pack.v    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index 6141af0c5..0e95e073c 100644
--- a/HB/common/log.elpi
+++ b/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
diff --git a/tests/hb_pack.v b/tests/hb_pack.v
index a73618ad1..67b32cc0b 100644
--- a/tests/hb_pack.v
+++ b/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.