diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /toplevel/indschemes.mli | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
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 *) |