From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 checker/modops.ml | 58 +++++++++++++++++++++++++++++--------------------------
 1 file changed, 31 insertions(+), 27 deletions(-)

(limited to 'checker/modops.ml')

diff --git a/checker/modops.ml b/checker/modops.ml
index b720fb62..c7ad0977 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -16,29 +18,29 @@ open Declarations
 (*i*)
 
 let error_not_a_constant l =
-  error ("\""^(Label.to_string l)^"\" is not a constant")
+  user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant"))
 
-let error_not_a_functor () = error "Application of not a functor"
+let error_not_a_functor () = user_err Pp.(str "Application of not a functor")
 
-let error_incompatible_modtypes _ _ = error "Incompatible module types"
+let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types")
 
 let error_not_match l _ =
-  error ("Signature components for label "^Label.to_string l^" do not match")
+  user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match"))
 
-let error_no_such_label l = error ("No such label "^Label.to_string l)
+let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l))
 
 let error_no_such_label_sub l l1 =
   let l1 = ModPath.to_string l1 in
-  error ("The field "^
-         Label.to_string l^" is missing in "^l1^".")
+  user_err Pp.(str ("The field "^
+         Label.to_string l^" is missing in "^l1^"."))
 
-let error_not_a_module_loc loc s =
-  user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module"))
+let error_not_a_module_loc ?loc s =
+  user_err ?loc  (str ("\""^Label.to_string s^"\" is not a module"))
 
-let error_not_a_module s = error_not_a_module_loc Loc.ghost s
+let error_not_a_module s = error_not_a_module_loc s
 
 let error_with_module () =
-  error "Unsupported 'with' constraint in module implementation"
+  user_err Pp.(str "Unsupported 'with' constraint in module implementation")
 
 let is_functor = function
   | MoreFunctor _ -> true
@@ -49,7 +51,7 @@ let destr_functor = function
   | NoFunctor _ -> error_not_a_functor ()
 
 let module_body_of_type mp mtb =
-  { mtb with mod_mp = mp; mod_expr = Abstract }
+  { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
@@ -83,27 +85,29 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      let u = 
-	if cb.const_polymorphic then
-	  Univ.make_abstract_instance cb.const_universes
-	else Univ.Instance.empty
+      let u =
+        match cb.const_universes with
+      | Monomorphic_const _ -> Univ.Instance.empty
+      | Polymorphic_const auctx -> Univ.make_abstract_instance auctx
       in
       { cb with
 	const_body = Def (Declarations.from_val (Const (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
-  else strengthen_body true mp_from mp_to mb
+  else
+    let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in
+    strengthen_body mk_expr mp_from mp_to mb
 
-and strengthen_body is_mod mp_from mp_to mb =
+and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun mk_expr mp_from mp_to mb ->
   match mb.mod_type with
   | MoreFunctor _ -> mb
   | NoFunctor sign ->
     let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
     in
     { mb with
-      mod_expr =
-        (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract);
+      mod_expr = mk_expr mp_to;
       mod_type = NoFunctor sign_out;
       mod_delta = resolve_out }
 
@@ -130,7 +134,7 @@ and strengthen_sig mp_from sign mp_to resolver =
 	resolve_out,item::rest'
 
 let strengthen mtb mp =
-  strengthen_body false mtb.mod_mp mp mtb
+  strengthen_body ignore mtb.mod_mp mp mtb
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
@@ -138,9 +142,9 @@ let subst_and_strengthen mb mp =
 let module_type_of_module mp mb =
   let mtb =
     { mb with
-      mod_expr = Abstract;
+      mod_expr = ();
       mod_type_alg = None;
-      mod_retroknowledge = [] }
+      mod_retroknowledge = ModTypeRK }
   in
   match mp with
   | Some mp -> strengthen {mtb with mod_mp = mp} mp
-- 
cgit v1.2.3