summaryrefslogtreecommitdiff
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 5ddc4452..1b66c334 100644
--- a/plugins/dp/Dp.v
+++ b/plugins/dp/Dp.v
@@ -6,8 +6,6 @@ Require Export Classical.
(* Zenon *)
(* Copyright 2004 INRIA *)
-(* $Id: Dp.v 12337 2009-09-17 15:58:14Z glondu $ *)
-
Lemma zenon_nottrue :
(~True -> False).
Proof. tauto. Qed.