Commits

Dmitry Grebeniuk  committed 396c5f1

DEBUG is now in global definitions; DEBUG definition changed from eq/eq_refl to True/I for simplicity

  • Participants
  • Parent commits 0af767b

Comments (0)

Files changed (1)

File Breakpoints.v

 Require Import String.
 Open Scope string_scope.
 
+Definition DEBUG {A} (a : A) := True.
+Global Opaque DEBUG.
+
+Ltac FINISH :=
+  match goal with
+  | |- DEBUG ?x => exact I
+  | _ => idtac
+  end
+.
+
+
 Module Named.
 
 Definition mytt : unit := tt.
   end
 .
 
-Definition DEBUG {A} (a : A) : Type.
-exact (a = a)
-.
-Defined.
-
 Global Opaque mytt.
 Global Opaque BREAK.
-Global Opaque DEBUG.
-
-Ltac FINISH :=
-  match goal with
-  | |- DEBUG ?x => exact eq_refl
-  | _ => idtac
-  end
-.
-
-Notation "'DEBUG' x" := (DEBUG x)
-  (at level 100)
-.
 
 
 Definition break_marked (lbl : string) {A} (a : A) := a.
 
 Module Nameless.
 
-Ltac FINISH :=
-  match goal with
-  | |- Named.DEBUG ?x => exact eq_refl
-  | _ => idtac
-  end
-.
-
-Notation "'DEBUG' x" := (Named.DEBUG x)
-  (at level 100)
-.
-
 Definition BREAK {A} (a : A) : A :=
   match Named.mytt with
   | tt => a
 End Nameless.
 
 
+Notation "'DEBUG' x" := (DEBUG x)
+  (at level 100)
+.