Merge branch 'v8.5'

8 files changed, 97 insertions, 52 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index cc7c4d7f11..a82f5260ba 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -950,7 +950,7 @@ type 'modast module_params =
 let debug_print_modtab _ =
   let pr_seg = function
     | [] -> str "[]"
-    | l -> str ("[." ^ string_of_int (List.length l) ^ ".]")
+    | l -> str "[." ++ int (List.length l) ++ str ".]"
   in
   let pr_modinfo mp (prefix,substobjs,keepobjs) s =
     s ++ str (string_of_mp mp) ++ (spc ())
diff --git a/library/goptions.ml b/library/goptions.ml
index ef25fa5902..4f50fbfbdd 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -35,7 +35,7 @@ type option_state = {
 let nickname table = String.concat " " table
 
 let error_undeclared_key key =
-  error ((nickname key)^": no table or option of this type")
+  errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
 
 (****************************************************************************)
 (* 1- Tables                                                                *)
@@ -301,7 +301,9 @@ let declare_string_option =
 let set_option_value locality check_and_cast key v =
   let (name, depr, (_,read,write,lwrite,gwrite)) =
     try get_option key
-    with Not_found -> error ("There is no option "^(nickname key)^".")
+    with Not_found ->
+      errorlabstrm "Goptions.set_option_value"
+        (str "There is no option " ++ str (nickname key) ++ str ".")
   in
   let write = match locality with
     | None -> write
@@ -364,9 +366,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg_info (str ("The "^name^" mode is "^(if b then "on" else "off")))
+	msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s))
+	msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
@@ -383,7 +385,7 @@ let get_tables () =
 
 let print_tables () =
   let print_option key name value depr =
-    let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
+    let msg = str "  " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
     if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
     else msg ++ fnl ()
   in
@@ -401,10 +403,10 @@ let print_tables () =
       !value_tab (mt ()) ++
   str "Tables:" ++ fnl () ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !string_table (mt ()) ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !ref_table (mt ()) ++
     fnl ()
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 4b0e2e3d1a..94f53219e7 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Globnames
+open Nameops
 open Term
 open Reduction
 open Declarations
@@ -337,10 +338,12 @@ let check_correct_manual_implicits autoimps l =
   List.iter (function
     | ExplByName id,(b,fi,forced) ->
 	if not forced then
-	  error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".")
+	  errorlabstrm ""
+            (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
     | ExplByPos (i,_id),_t ->
 	if i<1 || i>List.length autoimps then
-	  error ("Bad implicit argument number: "^(string_of_int i)^".")
+	  errorlabstrm ""
+            (str "Bad implicit argument number: " ++ int i ++ str ".")
 	else
 	  errorlabstrm ""
 	    (str "Cannot set implicit argument number " ++ int i ++
diff --git a/library/lib.ml b/library/lib.ml
index 9977b66654..81db547efd 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -75,7 +75,8 @@ let classify_segment seg =
     | (_,ClosedModule _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
-      error ("there are still opened " ^ module_kind ty ^"s")
+      errorlabstrm "Lib.classify_segment"
+        (str "there are still opened " ++ str (module_kind ty) ++ str "s")
     | (_,FrozenState _) :: stk -> clean acc stk
   in
     clean ([],[],[]) (List.rev seg)
@@ -274,7 +275,7 @@ let start_modtype = start_mod true None
 let error_still_opened string oname =
   let id = basename (fst oname) in
   errorlabstrm ""
-    (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.")
+    (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
 
 let end_mod is_type =
   let oname,fs =
@@ -318,7 +319,8 @@ let end_compilation_checks dir =
     try match snd (find_entry_p is_opening_node) with
       | OpenedSection _ -> error "There are some open sections."
       | OpenedModule (ty,_,_,_) ->
-	error ("There are some open "^module_kind ty^"s.")
+	errorlabstrm "Lib.end_compilation_checks"
+          (str "There are some open " ++ str (module_kind ty) ++ str "s.")
       | _ -> assert false
     with Not_found -> ()
   in
@@ -369,7 +371,8 @@ let find_opening_node id =
     let oname,entry = find_entry_p is_opening_node in
     let id' = basename (fst oname) in
     if not (Names.Id.equal id id') then
-      error ("Last block to end has name "^(Names.Id.to_string id')^".");
+      errorlabstrm "Lib.find_opening_node"
+        (str "Last block to end has name " ++ pr_id id' ++ str ".");
     entry
   with Not_found -> error "There is nothing to end."
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 5f2a2127d9..74930d76ec 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Libnames
+open Pp
 
 (* The relax flag is used to make it possible to load files while ignoring
    failures to incorporate some objects.  This can be useful when one
@@ -33,15 +34,13 @@ type 'a object_declaration = {
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
-let yell s = Errors.anomaly (Pp.str s)
-
 let default_object s = {
   object_name = s;
   cache_function = (fun _ -> ());
   load_function = (fun _ _ -> ());
   open_function = (fun _ _ -> ());
   subst_function = (fun _ ->
-    yell ("The object "^s^" does not know how to substitute!"));
+    Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
   classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
   rebuild_function = (fun x -> x)}
diff --git a/library/library.ml b/library/library.ml
index 9d0ccb972a..1ffa1a305c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -126,7 +126,8 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (DirPath.to_string dir))
+    errorlabstrm "Library.find_library"
+      (str "Unknown library " ++ str (DirPath.to_string dir))
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -378,10 +379,10 @@ let access_table what tables dp i =
       let t =
         try fetch_delayed f
         with Faulty f ->
-          error
-            ("The file "^f^" (bound to " ^ dir_path ^
-            ") is inaccessible or corrupted,\n" ^
-            "cannot load some "^what^" in it.\n")
+          errorlabstrm "Library.access_table"
+            (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
+             str ") is inaccessible or corrupted,\ncannot load some " ++
+             str what ++ str " in it.\n")
       in
       tables := LibraryMap.add dp (Fetched t) !tables;
       t
@@ -462,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
     errorlabstrm "load_physical_library"
-      (str ("The file " ^ f ^ " contains library") ++ spc () ++
+      (str "The file " ++ str f ++ str " contains library" ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
   Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
@@ -475,9 +476,7 @@ and intern_library_deps libs dir m from =
 and intern_mandatory_library caller from libs (dir,d) =
   let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
-      ".vo makes inconsistent assumptions over library " ^
-      DirPath.to_string dir));
+    errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
   libs
 
 let rec_intern_library libs mref =
@@ -487,7 +486,7 @@ let rec_intern_library libs mref =
 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 " ^ f ^ " contains library") ++ spc () ++
+      (str "The file " ++ str f ++ str " contains library" ++ spc () ++
       pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
       pr_id id)
   | _ -> ()
@@ -613,7 +612,7 @@ let safe_locate_module (loc,qid) =
   try Nametab.locate_module qid
   with Not_found ->
     user_err_loc
-      (loc,"import_library", str (string_of_qualid qid ^ " is not a module"))
+      (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -633,7 +632,12 @@ let import_module export modl =
           with Not_found-> flush acc; safe_locate_module m, [] in
         (match m with
         | MPfile dir -> aux (dir::acc) l
-        | mp -> flush acc; Declaremods.import_module export mp; aux [] l)
+        | mp ->
+            flush acc;
+            try Declaremods.import_module export mp; aux [] l
+            with Not_found ->
+              user_err_loc (loc,"import_library",
+                str (string_of_qualid dir) ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
@@ -645,8 +649,8 @@ let check_coq_overwriting p id =
   let is_empty = match l with [] -> true | _ -> false in
   if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
     errorlabstrm ""
-      (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
-      ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
+      (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+      str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
 
 (* Verifies that a string starts by a letter and do not contain
    others caracters than letters, digits, or `_` *)
@@ -790,7 +794,7 @@ let save_library_to ?todo dir f otab =
         msg_error (str"Could not compile the library to native code. Skipping.")
    with reraise ->
     let reraise = Errors.push reraise in
-    let () = msg_warning (str ("Removed file "^f')) in
+    let () = msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
diff --git a/library/universes.ml b/library/universes.ml
index 9fddc7067b..3a8ee26254 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -139,6 +139,32 @@ let eq_constr_univs_infer univs m n =
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
       res, !cstrs
 
+(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
+    to expose subterms of [m] and [n], arguments. *)
+let eq_constr_univs_infer_with kind1 kind2 univs m n =
+  (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
+     haven't find a way to factor the code without destroying
+     pointer-equality optimisations in [eq_constr_univs_infer].
+     Pointer equality is not sufficient to ensure equality up to
+     [kind1,kind2], because [kind1] and [kind2] may be different,
+     typically evaluating [m] and [n] in different evar maps. *)
+  let cstrs = ref Constraints.empty in
+  let eq_universes strict = Univ.Instance.check_eq univs in
+  let eq_sorts s1 s2 = 
+    if Sorts.equal s1 s2 then true
+    else
+      let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+      if Univ.check_eq univs u1 u2 then true
+      else
+	(cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+	 true)
+  in
+  let rec eq_constr' m n = 
+    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
+  in
+  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
+  res, !cstrs
+
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
@@ -148,18 +174,18 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-		true)
+	if Univ.check_eq univs u1 u2 then true
+	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+	      true)
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then true
-	  else
-	    (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
-	     true)
+	if Univ.check_leq univs u1 u2 then true
+	else
+	  (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -169,7 +195,7 @@ let leq_constr_univs_infer univs m n =
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let eq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -188,7 +214,7 @@ let eq_constr_universes m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 let leq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -216,22 +242,22 @@ let leq_constr_universes m n =
       Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let compare_head_gen_proj env equ eqs eqc' m n =
   match kind_of_term m, kind_of_term n with
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
-    (match kind_of_term f with
-    | Const (p', u) when eq_constant (Projection.constant p) p' -> 
-      let pb = Environ.lookup_projection p env in
-      let npars = pb.Declarations.proj_npars in
-	if Array.length args == npars + 1 then
-	  eqc' c args.(npars)
-	else false
-    | _ -> false)
+      (match kind_of_term f with
+      | Const (p', u) when eq_constant (Projection.constant p) p' -> 
+          let pb = Environ.lookup_projection p env in
+          let npars = pb.Declarations.proj_npars in
+	  if Array.length args == npars + 1 then
+	    eqc' c args.(npars)
+	  else false
+      | _ -> false)
   | _ -> Constr.compare_head_gen equ eqs eqc' m n
-    
+      
 let eq_constr_universes_proj env m n =
   if m == n then true, Constraints.empty
   else 
@@ -249,7 +275,7 @@ let eq_constr_universes_proj env m n =
       m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
     in
     let res = eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 (* Generator of levels *)
 let new_univ_level, set_remote_new_univ_level =
diff --git a/library/universes.mli b/library/universes.mli
index 252648d7dc..5527da0903 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -66,6 +66,14 @@ val to_constraints : universes -> universe_constraints -> constraints
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
 val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
 
+(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
+    {!eq_constr_univs_infer} taking kind-of-term functions, to expose
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  Univ.universes -> constr -> constr -> bool universe_constrained
+
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
     modulo alpha, casts, application grouping, the universe constraints
     in [u] and additional constraints [c]. *)