From 7ea13f14b30b74d644458464e3cd56d45b303f69 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 16 Dec 1999 15:01:07 +0000
Subject: bug : import -> export dans Require

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@260 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 280274788b..765f3e9f6e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1092,7 +1092,7 @@ let _ =
 		   else 
 		     Some (specif="SPECIFICATION"))
 		  (string_of_id id) None)
-      	       (import="IMPORT") 
+      	       (import="EXPORT") 
        | _ -> bad_vernac_args "Require")
 
 let _ =
@@ -1108,7 +1108,7 @@ let _ =
 		    else 
 		      Some (specif="SPECIFICATION"))
 		   (string_of_id id) (Some filename))
-		(import="IMPORT"))
+		(import="EXPORT"))
        | _ -> bad_vernac_args "RequireFrom")
 
 let _ =
-- 
cgit v1.2.3