More debug info in reification

2 files changed, 19 insertions, 27 deletions

diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v
index 810db4d9b..49d32824d 100644
--- a/src/Compilers/Reify.v
+++ b/src/Compilers/Reify.v
@@ -26,9 +26,9 @@ End ReifyDebugNotations.
 Ltac debug_enter_reify_idtac funname e :=
   let s := (eval compute in (String.append funname ": Attempting to reify:")) in
   cidtac2 s e.
-Ltac debug_leave_reify_success_idtac funname e :=
+Ltac debug_leave_reify_success_idtac funname e ret :=
   let s := (eval compute in (String.append funname ": Success in reifying:")) in
-  cidtac2 s e.
+  cidtac4 s e " as " ret.
 Ltac debug_leave_reify_failure_idtac funname e :=
   let s := (eval compute in (String.append funname ": Failure in reifying:")) in
   cfail2 s e.
@@ -60,12 +60,12 @@ Ltac debug3 tac :=
   | _ => check_debug_level_then_Set ()
   end.
 Ltac debug_enter_reify2 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e).
-Ltac debug_leave_reify3_success funname e := debug3 ltac:(fun _ => debug_leave_reify_success_idtac funname e).
+Ltac debug_leave_reify3_success funname e ret := debug3 ltac:(fun _ => debug_leave_reify_success_idtac funname e ret).
 Ltac debug_enter_reify3 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e).
 Ltac debug_enter_reify_flat_type e := debug_enter_reify3 "reify_flat_type" e.
 Ltac debug_enter_reify_type e := debug_enter_reify3 "reify_type" e.
 Ltac debug_enter_reifyf e := debug_enter_reify2 "reifyf" e.
-Ltac debug_leave_reifyf_success e := debug_leave_reify3_success "reifyf" e.
+Ltac debug_leave_reifyf_success e ret := debug_leave_reify3_success "reifyf" e ret.
 Ltac debug_leave_reifyf_failure e := debug_leave_reify_failure_idtac "reifyf" e.
 Ltac debug_reifyf_case case := debug3 ltac:(fun _ => debug_reifyf_case_idtac case).
 Ltac debug_enter_reify_abs e := debug_enter_reify2 "reify_abs" e.
@@ -314,7 +314,7 @@ Ltac reifyf base_type_code interp_base_type op var e :=
             => cfail2 "Failed to reify:"%string x
           end
         end in
-    let dummy := debug_leave_reifyf_success e in
+    let dummy := debug_leave_reifyf_success e ret in
     ret
   | _ => debug_leave_reifyf_failure e
   end.
diff --git a/src/Util/Tactics/DebugPrint.v b/src/Util/Tactics/DebugPrint.v
index b35a3e77f..5c16b4403 100644
--- a/src/Util/Tactics/DebugPrint.v
+++ b/src/Util/Tactics/DebugPrint.v
@@ -17,6 +17,8 @@ Class cidtac2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cidtac2 : True.
 Hint Extern 0 (cidtac2 ?msg1 ?msg2) => idtac msg1 msg2; exact I : typeclass_instances.
 Class cidtac3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cidtac3 : True.
 Hint Extern 0 (cidtac3 ?msg1 ?msg2 ?msg3) => idtac msg1 msg2 msg3; exact I : typeclass_instances.
+Class cidtac4 {T1 T2 T3 T4} (msg1 : T1) (msg2 : T2) (msg3 : T3) (msg4 : T4) := Build_cidtac4 : True.
+Hint Extern 0 (cidtac4 ?msg1 ?msg2 ?msg3 ?msg4) => idtac msg1 msg2 msg3 msg4; exact I : typeclass_instances.
 
 Class cfail {T} (msg : T) := Build_cfail : True.
 Hint Extern 0 (cfail ?msg) => idtac "Error:" msg; exact I : typeclass_instances.
@@ -25,36 +27,26 @@ Hint Extern 0 (cfail2 ?msg1 ?msg2) => idtac "Error:" msg1 msg2; exact I : typecl
 Class cfail3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cfail3 : True.
 Hint Extern 0 (cfail3 ?msg1 ?msg2 ?msg3) => idtac "Error:" msg1 msg2 msg3; exact I : typeclass_instances.
 
-Ltac cidtac msg :=
+Ltac constr_run_tac tac :=
   let dummy := match goal with
-               | _ => idtac msg
+               | _ => tac ()
                end in
   constr:(I).
+
+Ltac cidtac msg :=
+  constr_run_tac ltac:(fun _ => idtac msg).
 Ltac cidtac2 msg1 msg2 :=
-  let dummy := match goal with
-               | _ => idtac msg1 msg2
-               end in
-  constr:(I).
+  constr_run_tac ltac:(fun _ => idtac msg1 msg2).
 Ltac cidtac3 msg1 msg2 msg3 :=
-  let dummy := match goal with
-               | _ => idtac msg1 msg2 msg3
-               end in
-  constr:(I).
+  constr_run_tac ltac:(fun _ => idtac msg1 msg2 msg3).
+Ltac cidtac4 msg1 msg2 msg3 msg4 :=
+  constr_run_tac ltac:(fun _ => idtac msg1 msg2 msg3 msg4).
 Ltac cfail msg :=
-  let dummy := match goal with
-               | _ => idtac "Error:" msg
-               end in
-  constr:(I : I).
+  constr_run_tac ltac:(fun _ => idtac "Error:" msg).
 Ltac cfail2 msg1 msg2 :=
-  let dummy := match goal with
-               | _ => idtac "Error:" msg1 msg2
-               end in
-  constr:(I : I).
+  constr_run_tac ltac:(fun _ => idtac "Error:" msg1 msg2).
 Ltac cfail3 msg1 msg2 msg3 :=
-  let dummy := match goal with
-               | _ => idtac "Error:" msg1 msg2 msg3
-               end in
-  constr:(I : I).
+  constr_run_tac ltac:(fun _ => idtac "Error:" msg1 msg2 msg3).
 
 Ltac idtac_goal := lazymatch goal with |- ?G => idtac "Goal:" G end.
 Ltac idtac_context :=