From f4fdaa8991fa451656ba726f5a5e4e8f71d7ea20 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 5 Apr 2017 17:33:17 -0400 Subject: Don't clutter up typeclass log with cidtac Now that we depend on 8.5, we can use the fact that [match goal] forces early execution --- src/Util/Tactics/DebugPrint.v | 36 ++++++++++++++++++++++++++++++------ 1 file changed, 30 insertions(+), 6 deletions(-) (limited to 'src/Util/Tactics') diff --git a/src/Util/Tactics/DebugPrint.v b/src/Util/Tactics/DebugPrint.v index e1650f170..b35a3e77f 100644 --- a/src/Util/Tactics/DebugPrint.v +++ b/src/Util/Tactics/DebugPrint.v @@ -25,12 +25,36 @@ 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 := constr:(_ : cidtac msg). -Ltac cidtac2 msg1 msg2 := constr:(_ : cidtac2 msg1 msg2). -Ltac cidtac3 msg1 msg2 msg3 := constr:(_ : cidtac2 msg1 msg2 msg3). -Ltac cfail msg := let dummy := constr:(_ : cfail msg) in constr:(I : I). -Ltac cfail2 msg1 msg2 := let dummy := constr:(_ : cfail2 msg1 msg2) in constr:(I : I). -Ltac cfail3 msg1 msg2 msg3 := let dummy := constr:(_ : cfail2 msg1 msg2 msg3) in constr:(I : I). +Ltac cidtac msg := + let dummy := match goal with + | _ => idtac msg + end in + constr:(I). +Ltac cidtac2 msg1 msg2 := + let dummy := match goal with + | _ => idtac msg1 msg2 + end in + constr:(I). +Ltac cidtac3 msg1 msg2 msg3 := + let dummy := match goal with + | _ => idtac msg1 msg2 msg3 + end in + constr:(I). +Ltac cfail msg := + let dummy := match goal with + | _ => idtac "Error:" msg + end in + constr:(I : I). +Ltac cfail2 msg1 msg2 := + let dummy := match goal with + | _ => idtac "Error:" msg1 msg2 + end in + constr:(I : I). +Ltac cfail3 msg1 msg2 msg3 := + let dummy := match goal with + | _ => idtac "Error:" msg1 msg2 msg3 + end in + constr:(I : I). Ltac idtac_goal := lazymatch goal with |- ?G => idtac "Goal:" G end. Ltac idtac_context := -- cgit v1.2.3