Merge branch 'v8.5'

5 files changed, 28 insertions, 36 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c3181e4c75..8438380c9c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -28,9 +28,9 @@ open Decl_kinds
 
 (** flag for internal message display *)
 type internal_flag = 
-  | KernelVerbose (* kernel action, a message is displayed *)
-  | KernelSilent  (* kernel action, no message is displayed *)
-  | UserVerbose   (* user action, a message is displayed *)
+  | UserAutomaticRequest (* kernel action, a message is displayed *)
+  | InternalTacticRequest  (* kernel action, no message is displayed *)
+  | UserIndividualRequest   (* user action, a message is displayed *)
 
 (** Declaration of section variables and local definitions *)
 
@@ -253,7 +253,7 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let cd = (* We deal with side effects *)
     match cd with
     | Entries.DefinitionEntry de ->
@@ -283,7 +283,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?(internal=UserVerbose) 
+let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
   let cb = 
diff --git a/library/declare.mli b/library/declare.mli
index d8a00db0cf..76538a6248 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -43,9 +43,9 @@ type constant_declaration = constant_entry * logical_kind
    
    *)
 type internal_flag =
-  | KernelVerbose
-  | KernelSilent
-  | UserVerbose
+  | UserAutomaticRequest
+  | InternalTacticRequest
+  | UserIndividualRequest
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
diff --git a/library/library.ml b/library/library.ml
index f7ca4e9760..a09f91b15a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -488,18 +488,8 @@ let rec_intern_library libs mref =
   let _, libs = intern_library libs mref None in
   libs
 
-let check_library_short_name f dir = function
-  | Some id when not (Id.equal id (snd (split_dirpath dir))) ->
-      errorlabstrm "check_library_short_name"
-      (str "The file " ++ str f ++ str " contains library" ++ spc () ++
-      pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
-      pr_id id)
-  | _ -> ()
-
-let rec_intern_by_filename_only id f =
+let rec_intern_by_filename_only f =
   let m = try intern_from_file f with Sys_error s -> error s in
-  (* Only the base name is expected to match *)
-  check_library_short_name f m.library_name id;
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
@@ -518,12 +508,12 @@ let native_name_from_filename f =
   let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
-let rec_intern_library_from_file idopt f =
+let rec_intern_library_from_file f =
   (* A name is specified, we have to check it contains library id *)
   let paths = Loadpath.get_paths () in
   let _, f =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
-  rec_intern_by_filename_only idopt f
+  rec_intern_by_filename_only f
 
 (**********************************************************************)
 (*s [require_library] loads and possibly opens a library. This is a
@@ -600,8 +590,8 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library_from_file idopt file export =
-  let modref,needed = rec_intern_library_from_file idopt file in
+let require_library_from_file file export =
+  let modref,needed = rec_intern_library_from_file file in
   let needed = List.rev_map snd needed in
   if Lib.is_module_or_modtype () then begin
     add_anonymous_leaf (in_require (needed,[modref],None));
@@ -678,22 +668,22 @@ let check_module_name s =
     | c -> err c
 
 let start_library f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let () = if not (Sys.file_exists f) then
+    errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
+  in
   let ldir0 =
     try
-      let lp = Loadpath.find_load_path (Filename.dirname longf) in
+      let lp = Loadpath.find_load_path (Filename.dirname f) in
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let file = Filename.basename f in
+  let file = Filename.chop_extension (Filename.basename f) in
   let id = Id.of_string file in
   check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
-  ldir,longf
+  ldir
 
 let load_library_todo f =
   let paths = Loadpath.get_paths () in
diff --git a/library/library.mli b/library/library.mli
index 967a54e4c8..3d96f9a751 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,10 +22,9 @@ open Libnames
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
-val require_library_from_file :
-  Id.t option -> CUnix.physical_path -> bool option -> unit
+val require_library_from_file : CUnix.physical_path -> bool option -> unit
 
-(** {6 ... } *)
+(** {6 Start the compilation of a library } *)
 
 (** Segments of a library *)
 type seg_sum
@@ -39,10 +38,12 @@ type seg_proofs = Term.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located list -> unit
 
-(** {6 Start the compilation of a library } *)
-val start_library : string -> DirPath.t * string
+(** Start the compilation of a file as a library. The argument must be an
+    existing file on the system, and the returned path is the associated
+    absolute logical path of the library. *)
+val start_library : CUnix.physical_path -> DirPath.t
 
-(** {6 End the compilation of a library and save it to a ".vo" file } *)
+(** End the compilation of a library and save it to a ".vo" file *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
diff --git a/library/nametab.ml b/library/nametab.ml
index 6af1e686b0..5b6d7cd982 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -524,7 +524,8 @@ let shortest_qualid_of_tactic kn =
 
 let pr_global_env env ref =
   try str (string_of_qualid (shortest_qualid_of_global env ref))
-  with Not_found as e -> prerr_endline "pr_global_env not found"; raise e
+  with Not_found as e ->
+    if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
 
 let global_inductive r =
   match global r with