Utilisation de try_locate_qualified_library au lieu de locate_qualified_library (suite commit #11177)

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

6 files changed, 13 insertions, 10 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6c09e4acef..d2c2b0d6a8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -250,7 +250,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
 let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ntn,args = contract_notation ntn args in
   let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-    if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.ntn_loc loc args ntn) df;
+    if !Flags.dump then Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
     let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
       subst_aconstr_in_rawconstr loc intern subst ([],env) c
 
@@ -616,7 +616,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
       let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-      if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.patntn_loc loc args ntn) df;
+      if !Flags.dump then Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes 
 	c
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 3e28307e0e..84117fafa4 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -207,13 +207,6 @@ let dump_libref loc dp ty =
     dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
 			     (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
-let loc_of_notation f loc args ntn =
-  if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
-  else snd (Util.unloc (f (List.hd args)))
-
-let ntn_loc = loc_of_notation Topconstr.constr_loc
-let patntn_loc = loc_of_notation Topconstr.cases_pattern_expr_loc
-
 let dump_notation_location pos ((path,df),sc) =
   let rec next growing =
     let loc = Lexer.location_function !token_number in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 570eae7e56..8ded0a35bd 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -947,3 +947,10 @@ type module_type_ast =
 type include_ast =
   | CIMTE of module_type_ast
   | CIME of module_ast
+
+let loc_of_notation f loc args ntn =
+  if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
+  else snd (Util.unloc (f (List.hd args)))
+
+let ntn_loc = loc_of_notation constr_loc
+let patntn_loc = loc_of_notation cases_pattern_expr_loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 46133c27bc..aed67975dd 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -240,3 +240,5 @@ type include_ast =
   | CIMTE of module_type_ast
   | CIME of module_ast
 
+val ntn_loc : Util.loc -> constr_expr list -> string -> int
+val patntn_loc : Util.loc -> cases_pattern_expr list -> string -> int
diff --git a/library/library.mli b/library/library.mli
index d7cef32435..ec911fc0f7 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -76,6 +76,7 @@ type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
   bool -> qualid -> library_location * dir_path * System.physical_path
+val try_locate_qualified_library : qualid located -> dir_path * string
 
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c882d2108f..4d7300833a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -571,7 +571,7 @@ let vernac_end_segment lid =
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
-  let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library false qid) in dp) qidl in
+  let modrefl = List.map (fun qid -> let (dp, _) = (Library.try_locate_qualified_library qid) in dp) qidl in
     List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl;
     Library.require_library qidl import