diff options
Diffstat (limited to 'toplevel/indschemes.mli')
| -rw-r--r-- | toplevel/indschemes.mli | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index f6eb4fe1..98746107 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -1,20 +1,17 @@ (************************************************************************) (* 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 *) (************************************************************************) -open Util +open Loc open Names open Term open Environ -open Libnames -open Glob_term -open Genarg open Vernacexpr -open Ind_tables +open Misctypes (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *) @@ -35,17 +32,17 @@ val declare_rewriting_schemes : inductive -> unit (** Mutual Minimality/Induction scheme *) val do_mutual_induction_scheme : - (identifier located * bool * inductive * glob_sort) list -> unit + (Id.t located * bool * inductive * glob_sort) list -> unit (** Main calls to interpret the Scheme command *) -val do_scheme : (identifier located option * scheme) list -> unit +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 -> constr * types -val do_combined_scheme : identifier located -> identifier located list -> unit +val do_combined_scheme : Id.t located -> Id.t located list -> unit (** Hook called at each inductive type definition *) |