diff options
| author | Emilio Jesus Gallego Arias | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /tactics/ind_tables.mli | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
Diffstat (limited to 'tactics/ind_tables.mli')
| -rw-r--r-- | tactics/ind_tables.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index f825c4f4a3..232a193ac3 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -20,7 +20,7 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> 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 * Safe_typing.private_constants @@ -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 * Safe_typing.private_constants + Id.t option -> inductive -> Constant.t * Safe_typing.private_constants val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants + (int * Id.t) list -> MutInd.t -> Constant.t 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 * Safe_typing.private_constants +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants val check_scheme : 'a scheme_kind -> inductive -> bool |