diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 16:44:20 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-14 16:44:29 -0400 |
| commit | 7af112e5c46bc915b3209d28184ef2f90bf37aef (patch) | |
| tree | 7ef4824b966cf2c3be8def7c810b90846c0b9ebc /src/Util/Tactics | |
| parent | a6e0ab7466b2f8a717af2a463edc1d72eab99b5e (diff) | |
More debug info in reification
Diffstat (limited to 'src/Util/Tactics')
| -rw-r--r-- | src/Util/Tactics/DebugPrint.v | 36 |
1 files changed, 14 insertions, 22 deletions
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 := |