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

---
 kernel/modops.mli | 38 ++++++++++++++++++++------------------
 1 file changed, 20 insertions(+), 18 deletions(-)

(limited to 'kernel/modops.mli')

diff --git a/kernel/modops.mli b/kernel/modops.mli
index e9f3db6e..1db489e6 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -1,13 +1,15 @@
 (************************************************************************)
-(*  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)         *)
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Declarations
 open Entries
@@ -26,9 +28,9 @@ val destr_nofunctor : ('ty,'a) functorize -> 'a
 (** Conversions between [module_body] and [module_type_body] *)
 
 val module_type_of_module : module_body -> module_type_body
-val module_body_of_type : module_path -> module_type_body -> module_body
+val module_body_of_type : ModPath.t -> module_type_body -> module_body
 
-val check_modpath_equiv : env -> module_path -> module_path -> unit
+val check_modpath_equiv : env -> ModPath.t -> ModPath.t -> unit
 
 val implem_smartmap :
   (module_signature -> module_signature) ->
@@ -43,7 +45,7 @@ val subst_structure : substitution -> structure_body -> structure_body
 (** {6 Adding to an environment } *)
 
 val add_structure :
-  module_path -> structure_body -> delta_resolver -> env -> env
+  ModPath.t -> structure_body -> delta_resolver -> env -> env
 
 (** adds a module and its components, but not the constraints *)
 val add_module : module_body -> env -> env
@@ -53,19 +55,19 @@ the native compiler. The linking information is updated. *)
 val add_linked_module : module_body -> Pre_env.link_info -> env -> env
 
 (** same, for a module type *)
-val add_module_type : module_path -> module_type_body -> env -> env
+val add_module_type : ModPath.t -> module_type_body -> env -> env
 
 (** {6 Strengthening } *)
 
-val strengthen : module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> ModPath.t -> module_type_body
 
 val inline_delta_resolver :
-  env -> inline -> module_path -> MBId.t -> module_type_body ->
+  env -> inline -> ModPath.t -> MBId.t -> module_type_body ->
   delta_resolver -> delta_resolver
 
-val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
+val strengthen_and_subst_mb : module_body -> ModPath.t -> bool -> module_body
 
-val subst_modtype_and_resolver : module_type_body -> module_path ->
+val subst_modtype_and_resolver : module_type_body -> ModPath.t ->
   module_type_body
 
 (** {6 Cleaning a module expression from bounded parts }
@@ -94,6 +96,7 @@ type signature_mismatch_error =
   | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
   | NotConvertibleTypeField of env * types * types
+  | CumulativeStatusExpected of bool
   | PolymorphicStatusExpected of bool
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
@@ -103,11 +106,10 @@ type signature_mismatch_error =
   | RecordFieldExpected of bool
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
-  | NoTypeConstraintExpected
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.constraints
+  | IncompatibleConstraints of Univ.AUContext.t
 
 type module_typing_error =
   | SignatureMismatch of
@@ -117,7 +119,7 @@ type module_typing_error =
   | NotAFunctor
   | IsAFunctor
   | IncompatibleModuleTypes of module_type_body * module_type_body
-  | NotEqualModulePaths of module_path * module_path
+  | NotEqualModulePaths of ModPath.t * ModPath.t
   | NoSuchLabel of Label.t
   | IncompatibleLabels of Label.t * Label.t
   | NotAModule of string
@@ -126,7 +128,7 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
-  | IncludeRestrictedFunctor of module_path
+  | IncludeRestrictedFunctor of ModPath.t
 
 exception ModuleTypingError of module_typing_error
 
@@ -152,4 +154,4 @@ val error_generative_module_expected : Label.t -> 'a
 
 val error_no_such_label_sub : Label.t->string->'a
 
-val error_include_restricted_functor : module_path -> 'a
+val error_include_restricted_functor : ModPath.t -> 'a
-- 
cgit v1.2.3