diff options
Diffstat (limited to 'toplevel/indschemes.mli')
| -rw-r--r-- | toplevel/indschemes.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index be49f41e5..7abae933d 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -7,15 +7,10 @@ (************************************************************************) open Loc -open Pp 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, ... *) |