Modification Require From

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3376 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 15 insertions, 10 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index a8d74c30e1..26026b6cd1 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -114,11 +114,11 @@ let execute_when_necessary v =
        with _ ->
 	 let l=prlist_with_sep spc pr_reference l in
 	 msgnl (str "Reinterning of " ++ l ++ str " failed"))
-  | VernacRequireFrom (_,_,name,_) ->
+  | VernacRequireFrom (_,_,f) ->
       (try 
 	Vernacentries.interp v
        with _ ->
-	 msgnl (str "Reinterning of " ++ Nameops.pr_id name ++ str " failed"))
+	 msgnl (str "Reinterning of " ++ Util.pr_str f ++ str " failed"))
   | _ -> ()); v;;
 
 let parse_to_dot =
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e58b7ffa4c..1c139ca8ea 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1437,8 +1437,10 @@ let xlate_vernac =
         CT_coerce_NONE_to_STRING_OPT CT_none)
    | VernacRequire (_,_,([]|_::_::_)) ->
        xlate_error "TODO: general form of future Require"
-   | VernacRequireFrom (impexp, spec, id, filename) ->
-      let ct_impexp, ct_spec = get_require_flags impexp spec in
+   | VernacRequireFrom (impexp, spec, filename) ->
+      let ct_impexp, ct_spec = get_require_flags impexp spec 
+      and id = id_of_string (Filename.basename filename)
+      in
       CT_require
        (ct_impexp, ct_spec, xlate_ident id, 
          CT_coerce_STRING_to_STRING_OPT (CT_string filename))
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e94b513fb4..30c0d368be 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -467,9 +467,12 @@ GEXTEND Gram
 	  VernacRequire (None, None, qidl)
       | IDENT "Require"; export = export_token; specif = specif_token;
         qidl = LIST1 global -> VernacRequire (Some export, specif, qidl)
-      | IDENT "Require"; export = export_token; specif = specif_token;
+(*      | IDENT "Require"; export = export_token; specif = specif_token;
         id = base_ident; filename = STRING -> 
-	  VernacRequireFrom (export, specif, id, filename)
+	  VernacRequireFrom (export, specif, id, filename) *)
+      | IDENT "Require"; export = export_token; specif = specif_token;
+        filename = STRING -> 
+	  VernacRequireFrom (export, specif, filename)
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING ->
 	  VernacDeclareMLModule l
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9b977b846f..c911633e82 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -558,8 +558,8 @@ let vernac_solve_existential = instantiate_nth_evar_com
 (*****************************)
 (* Auxiliary file management *)
 
-let vernac_require_from export spec id filename =
-  Library.require_library_from_file spec (Some id) filename export
+let vernac_require_from export spec filename =
+  Library.require_library_from_file spec None filename export
 
 let vernac_add_loadpath isrec pdir ldiropt =
   let alias = match ldiropt with
@@ -1077,7 +1077,7 @@ let interp c = match c with
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
   (* Auxiliary file and library management *)
-  | VernacRequireFrom (exp,spec,id,f) -> vernac_require_from exp spec id f
+  | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f
   | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias
   | VernacRemoveLoadPath s -> vernac_remove_loadpath s
   | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 36c277b953..a11eadc7ec 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -203,7 +203,7 @@ type vernac_expr =
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
-  | VernacRequireFrom of export_flag * specif_flag option * identifier * string
+  | VernacRequireFrom of export_flag * specif_flag option * string
   | VernacAddLoadPath of rec_flag * string * dir_path option
   | VernacRemoveLoadPath of string
   | VernacAddMLPath of rec_flag * string