diff options
Diffstat (limited to 'checker/modops.mli')
| -rw-r--r-- | checker/modops.mli | 29 |
1 files changed, 9 insertions, 20 deletions
diff --git a/checker/modops.mli b/checker/modops.mli index 61b2c80f..e22c2656 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -1,36 +1,31 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open Util open Names -open Univ -open Term -open Declarations +open Cic open Environ (*i*) (* Various operations on modules and module types *) -(* make the envirconment entry out of type *) -val module_body_of_type : module_path -> module_type_body -> module_body +val module_type_of_module : + module_path option -> module_body -> module_type_body -val module_type_of_module : module_path option -> module_body -> - module_type_body +val is_functor : ('ty,'a) functorize -> bool -val destr_functor : - env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body - -val add_signature : module_path -> structure_body -> delta_resolver -> env -> env +val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize (* adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env +val add_module_type : module_path -> module_type_body -> env -> env + val strengthen : module_type_body -> module_path -> module_type_body val subst_and_strengthen : module_body -> module_path -> module_body @@ -40,19 +35,13 @@ val error_incompatible_modtypes : val error_not_match : label -> structure_field_body -> 'a -val error_with_incorrect : label -> 'a +val error_with_module : unit -> 'a val error_no_such_label : label -> 'a val error_no_such_label_sub : label -> module_path -> 'a -val error_signature_expected : struct_expr_body -> 'a - val error_not_a_constant : label -> 'a val error_not_a_module : label -> 'a - -val error_a_generative_module_expected : label -> 'a - -val error_application_to_not_path : struct_expr_body -> 'a |