diff options
Diffstat (limited to 'plugins/dp')
| -rw-r--r-- | plugins/dp/Dp.v | 2 | ||||
| -rw-r--r-- | plugins/dp/g_dp.ml4 | 2 | ||||
| -rw-r--r-- | plugins/dp/zenon.v | 2 |
3 files changed, 0 insertions, 6 deletions
diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v index bc7d73f62d..1b66c334eb 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. diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 index 82f86cd81a..e2cd4b3e3e 100644 --- a/plugins/dp/g_dp.ml4 +++ b/plugins/dp/g_dp.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Dp TACTIC EXTEND Simplify diff --git a/plugins/dp/zenon.v b/plugins/dp/zenon.v index 502465c6be..89028c4f4c 100644 --- a/plugins/dp/zenon.v +++ b/plugins/dp/zenon.v @@ -1,6 +1,4 @@ (* Copyright 2004 INRIA *) -(* $Id$ *) - Require Export Classical. Lemma zenon_nottrue : |