diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 3ba32da3c..56bdc810d 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -13,9 +13,10 @@ open Tacmach open Errors open Util open Pp +open Term +open Vars open Termops open Declarations -open Term open Names open Globnames open Inductiveops |