diff options
Diffstat (limited to 'vernac/indschemes.mli')
| -rw-r--r-- | vernac/indschemes.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 076e4938f..91c4c5825 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -11,7 +11,6 @@ open Names open Term open Environ open Vernacexpr -open Misctypes (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *) @@ -32,7 +31,7 @@ val declare_rewriting_schemes : inductive -> unit (** Mutual Minimality/Induction scheme *) val do_mutual_induction_scheme : - (Id.t located * bool * inductive * glob_sort) list -> unit + (Id.t located * bool * inductive * Sorts.family) list -> unit (** Main calls to interpret the Scheme command *) |