diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 13:04:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 13:11:38 +0100 |
| commit | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (patch) | |
| tree | 0b14bafe702a6219d960111148ff3a0cdc9e18e6 /toplevel/ind_tables.mli | |
| parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
| parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel/ind_tables.mli')
| -rw-r--r-- | toplevel/ind_tables.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index d0844dd94..abd951c31 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -20,9 +20,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants (** Main functions to register a scheme builder *) @@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Declareops.side_effects + Id.t option -> inductive -> constant * Safe_typing.private_constants val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects + (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants val check_scheme : 'a scheme_kind -> inductive -> bool |