From 5129c5b02bcab1426636d18583ec7a4a46195f0a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 2 Jan 2016 16:55:03 +0100
Subject: Reduce dependencies of interface files.

---
 pretyping/nativenorm.mli | 1 -
 pretyping/patternops.mli | 1 -
 pretyping/vnorm.mli      | 1 -
 printing/pptacticsig.mli | 2 --
 stm/lemmas.mli           | 2 --
 tactics/auto.mli         | 1 -
 tactics/eauto.mli        | 1 -
 tactics/tacintern.mli    | 1 -
 toplevel/assumptions.mli | 1 -
 9 files changed, 11 deletions(-)

diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 0352038385..286cb2e079 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -8,7 +8,6 @@
 open Term
 open Environ
 open Evd
-open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 0148280287..34191db344 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Context
 open Term
 open Globnames
 open Glob_term
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 9421b2d859..b75fe7c928 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Environ
-open Evd
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 01f240f6b8..5b89266553 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -8,11 +8,9 @@
 
 open Pp
 open Genarg
-open Constrexpr
 open Tacexpr
 open Ppextend
 open Environ
-open Pattern
 open Misctypes
 
 module type Pp = sig
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index e2ddf79df8..93f24b42cb 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -9,8 +9,6 @@
 open Names
 open Term
 open Decl_kinds
-open Constrexpr
-open Vernacexpr
 open Pfedit
 
 type 'a declaration_hook
diff --git a/tactics/auto.mli b/tactics/auto.mli
index eca592ad6b..3e05d88217 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -10,7 +10,6 @@ open Names
 open Term
 open Clenv
 open Pattern
-open Evd
 open Decl_kinds
 open Hints
 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 8e20793c46..985c08f93f 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Proof_type
-open Evd
 open Hints
 
 val hintbases : hint_db_name list option Pcoq.Gram.entry
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index a6e28d568d..1124756948 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -12,7 +12,6 @@ open Tacexpr
 open Genarg
 open Constrexpr
 open Misctypes
-open Nametab
 
 (** Globalization of tactic expressions :
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index 9c9f81bd2f..f89b395439 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
 open Globnames
-- 
cgit v1.2.3