aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/dp/Dp.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/dp/Dp.v')
-rw-r--r--plugins/dp/Dp.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v
index bc7d73f62..1b66c334e 100644
--- a/plugins/dp/Dp.v
+++ b/plugins/dp/Dp.v
@@ -6,8 +6,6 @@ Require Export Classical.
(* Zenon *)
(* Copyright 2004 INRIA *)
-(* $Id$ *)
-
Lemma zenon_nottrue :
(~True -> False).
Proof. tauto. Qed.