From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- vernac/indschemes.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac/indschemes.mli') diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 91c4c5825..659f12936 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -16,9 +16,9 @@ open Vernacexpr (** Build and register the boolean equalities associated to an inductive type *) -val declare_beq_scheme : mutual_inductive -> unit +val declare_beq_scheme : MutInd.t -> unit -val declare_eq_decidability : mutual_inductive -> unit +val declare_eq_decidability : MutInd.t -> unit (** Build and register a congruence scheme for an equality-like inductive type *) @@ -39,10 +39,10 @@ val do_scheme : (Id.t located option * scheme) list -> unit (** Combine a list of schemes into a conjunction of them *) -val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types +val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types val do_combined_scheme : Id.t located -> Id.t located list -> unit (** Hook called at each inductive type definition *) -val declare_default_schemes : mutual_inductive -> unit +val declare_default_schemes : MutInd.t -> unit -- cgit v1.2.3