aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/CheckerMaker.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/CheckerMaker.v')
-rw-r--r--plugins/micromega/CheckerMaker.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v
index 93b4d213f8..632280d5d8 100644
--- a/plugins/micromega/CheckerMaker.v
+++ b/plugins/micromega/CheckerMaker.v
@@ -12,6 +12,8 @@
(* *)
(************************************************************************)
+(* FK: scheduled for deletion *)
+(*
Require Import Setoid.
Require Import Decidable.
Require Import List.
@@ -127,3 +129,4 @@ apply <- negate_correct. intro; now elim H3. exact (H1 H2).
Qed.
End CheckerMaker.
+*) \ No newline at end of file