Don't force [Require Import String] for debug msgs

2 files changed, 29 insertions, 32 deletions

diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v
index 49d32824d..b9c958123 100644
--- a/src/Compilers/Reify.v
+++ b/src/Compilers/Reify.v
@@ -23,52 +23,44 @@ Module Import ReifyDebugNotations.
   Open Scope string_scope.
 End ReifyDebugNotations.
 
-Ltac debug_enter_reify_idtac funname e :=
-  let s := (eval compute in (String.append funname ": Attempting to reify:")) in
-  cidtac2 s e.
-Ltac debug_leave_reify_success_idtac funname e ret :=
-  let s := (eval compute in (String.append funname ": Success in reifying:")) in
-  cidtac4 s e " as " ret.
-Ltac debug_leave_reify_failure_idtac funname e :=
-  let s := (eval compute in (String.append funname ": Failure in reifying:")) in
-  cfail2 s e.
-Ltac debug_reifyf_case_idtac case :=
-  let s := (eval compute in (String.append "reifyf: " case)) in
-  cidtac s.
+Tactic Notation "debug_enter_reify_idtac" string(funname) uconstr(e)
+  := constr_run_tac ltac:(fun _ => idtac funname "Attempting to reify:" e).
+Tactic Notation "debug_leave_reify_success_idtac" string(funname) uconstr(e) uconstr(ret)
+  := constr_run_tac ltac:(fun _ => idtac funname "Success in reifying:" e "as" ret).
+Tactic Notation "debug_leave_reify_failure_idtac" string(funname) uconstr(e)
+  := constr_run_tac ltac:(fun _ => idtac funname "Failure in reifying:" e).
 Ltac check_debug_level_then_Set _ :=
   let lvl := reify_debug_level in
   lazymatch type of lvl with
   | nat => constr:(Set)
-  | ?T => cfail2 "reify_debug_level should have type nat but instead has type" T
+  | ?T => constr_run_tac ltac:(fun _ => idtac "Error: reify_debug_level should have type nat but instead has type" T)
   end.
 Ltac debug1 tac :=
   let lvl := reify_debug_level in
-  match lvl with
-  | S _ => tac ()
+  lazymatch lvl with
+  | S _ => constr_run_tac tac
   | _ => check_debug_level_then_Set ()
   end.
 Ltac debug2 tac :=
   let lvl := reify_debug_level in
-  match lvl with
-  | S (S _) => tac ()
+  lazymatch lvl with
+  | S (S _) => constr_run_tac tac
   | _ => check_debug_level_then_Set ()
   end.
 Ltac debug3 tac :=
   let lvl := reify_debug_level in
-  match lvl with
-  | S (S (S _)) => tac ()
+  lazymatch lvl with
+  | S (S (S _)) => constr_run_tac tac
   | _ => check_debug_level_then_Set ()
   end.
-Ltac debug_enter_reify2 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e).
-Ltac debug_leave_reify3_success funname e ret := debug3 ltac:(fun _ => debug_leave_reify_success_idtac funname e ret).
-Ltac debug_enter_reify3 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e).
-Ltac debug_enter_reify_flat_type e := debug_enter_reify3 "reify_flat_type" e.
-Ltac debug_enter_reify_type e := debug_enter_reify3 "reify_type" e.
-Ltac debug_enter_reifyf e := debug_enter_reify2 "reifyf" e.
-Ltac debug_leave_reifyf_success e ret := debug_leave_reify3_success "reifyf" e ret.
-Ltac debug_leave_reifyf_failure e := debug_leave_reify_failure_idtac "reifyf" e.
-Ltac debug_reifyf_case case := debug3 ltac:(fun _ => debug_reifyf_case_idtac case).
-Ltac debug_enter_reify_abs e := debug_enter_reify2 "reify_abs" e.
+Ltac debug_enter_reify_flat_type e := debug2 ltac:(fun _ => debug_enter_reify_idtac "reify_flat_type:" e).
+Ltac debug_enter_reify_type e := debug2 ltac:(fun _ => debug_enter_reify_idtac "reify_type:" e).
+Ltac debug_enter_reifyf e := debug2 ltac:(fun _ => debug_enter_reify_idtac "reifyf:" e).
+Ltac debug_leave_reifyf_success e ret := debug3 ltac:(fun _ => debug_leave_reify_success_idtac "reifyf:" e ret).
+Ltac debug_leave_reifyf_failure e := debug_leave_reify_failure_idtac "reifyf:" e.
+Tactic Notation "debug_reifyf_case" string(case)
+  := debug3 ltac:(fun _ => idtac "reifyf:" case).
+Ltac debug_enter_reify_abs e := debug2 ltac:(fun _ => debug_enter_reify_idtac "reify_abs:" e).
 
 Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T.
 Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False.
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 :=