diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-15 17:05:19 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-15 17:05:19 -0400 |
commit | 33acf79b3708da3a319d66f43f4671925fb83e55 (patch) | |
tree | 702d69f7f559d676dc8eb5d2d16bfb6673d0c40d /src/Util | |
parent | c41720ac3b505fd067538e03a8504cfade377a32 (diff) |
Don't force [Require Import String] for debug msgs
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Tactics/DebugPrint.v | 11 |
1 files changed, 8 insertions, 3 deletions
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 := |