diff options
Diffstat (limited to 'toplevel/auto_ind_decl.mli')
| -rw-r--r-- | toplevel/auto_ind_decl.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 660f6f7e7..6509a7d3b 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -8,10 +8,6 @@ open Term open Names -open Libnames -open Mod_subst -open Context -open Proof_type open Ind_tables (** This file is about the automatic generation of schemes about |