aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-05 21:08:12 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-05 21:08:12 +0000
commiteb196f1e86b446bffc9a2fff672be2f3fd589182 (patch)
tree3c0e959caa0a6146b378f4d5ff93a2eb8ca23283 /theories
parent6ef4bfcc3bfb5bbccb3638ef807d44766a139036 (diff)
Plus besoin de rajouter "Require Plus"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@803 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rwxr-xr-xtheories/Arith/Euclid_proof.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Arith/Euclid_proof.v b/theories/Arith/Euclid_proof.v
index 53dc4fc2e..b8863ad65 100755
--- a/theories/Arith/Euclid_proof.v
+++ b/theories/Arith/Euclid_proof.v
@@ -1,7 +1,6 @@
(* $Id$ *)
-Require Plus.
Require Minus.
Require Euclid_def.
Require Compare_dec.