From 7af112e5c46bc915b3209d28184ef2f90bf37aef Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 14 May 2017 16:44:20 -0400
Subject: More debug info in reification

---
 src/Util/Tactics/DebugPrint.v | 36 ++++++++++++++----------------------
 1 file changed, 14 insertions(+), 22 deletions(-)

(limited to 'src/Util/Tactics')

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 :=
-- 
cgit v1.2.3