diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 38 |
1 files changed, 20 insertions, 18 deletions
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 |