Modification Require From

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

2 files changed, 6 insertions, 4 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index a8d74c30e..26026b6cd 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 e58b7ffa4..1c139ca8e 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))