From 33acf79b3708da3a319d66f43f4671925fb83e55 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 15 Jun 2017 17:05:19 -0400 Subject: Don't force [Require Import String] for debug msgs --- src/Util/Tactics/DebugPrint.v | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'src/Util/Tactics') diff --git a/src/Util/Tactics/DebugPrint.v b/src/Util/Tactics/DebugPrint.v index 5c16b4403..3ced23331 100644 --- a/src/Util/Tactics/DebugPrint.v +++ b/src/Util/Tactics/DebugPrint.v @@ -32,6 +32,11 @@ Ltac constr_run_tac tac := | _ => tac () end in constr:(I). +Ltac constr_run_tac_fail tac := + let dummy := match goal with + | _ => tac () + end in + constr:(I : I). Ltac cidtac msg := constr_run_tac ltac:(fun _ => idtac msg). @@ -42,11 +47,11 @@ Ltac cidtac3 msg1 msg2 msg3 := Ltac cidtac4 msg1 msg2 msg3 msg4 := constr_run_tac ltac:(fun _ => idtac msg1 msg2 msg3 msg4). Ltac cfail msg := - constr_run_tac ltac:(fun _ => idtac "Error:" msg). + constr_run_tac_fail ltac:(fun _ => idtac "Error:" msg). Ltac cfail2 msg1 msg2 := - constr_run_tac ltac:(fun _ => idtac "Error:" msg1 msg2). + constr_run_tac_fail ltac:(fun _ => idtac "Error:" msg1 msg2). Ltac cfail3 msg1 msg2 msg3 := - constr_run_tac ltac:(fun _ => idtac "Error:" msg1 msg2 msg3). + constr_run_tac_fail 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