Merge branch 'v8.5'

11 files changed, 0 insertions, 12 deletions

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 53f8b0db8c..b6c5d426f9 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -12,7 +12,6 @@ open Names
 open Term
 open Context
 open Environ
-open Mod_subst
 
 (** {5 Existential variables and unification states}
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 7f7f4d7649..95a6ba79db 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -11,7 +11,6 @@ open Util
 open Errors
 open Names
 open Locus
-open Context
 open Term
 open Nameops
 open Termops
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 82330b8468..47d9654e57 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Locus
 open Context
 open Term
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 654f914b61..adf714db35 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -18,7 +18,6 @@ open Declarations
 open Declareops
 open Environ
 open Reductionops
-open Inductive
 
 (* The following three functions are similar to the ones defined in
    Inductive, but they expect an env *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b4e0459c1d..1106fefa39 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,7 +23,6 @@ open Reductionops
 open Cbv
 open Patternops
 open Locus
-open Pretype_errors
 
 (* Errors *)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5862a8525d..9f04faa839 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -15,7 +15,6 @@ open Term
 open Vars
 open Context
 open Environ
-open Locus
 
 (* Sorts and sort family *)
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9f3efd72bd..2552c67e61 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -11,7 +11,6 @@ open Names
 open Term
 open Context
 open Environ
-open Locus
 
 (** printers *)
 val print_sort : sorts -> std_ppcmds
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 817d687823..b64ccf60dd 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -14,7 +14,6 @@ open Term
 open Vars
 open Context
 open Evd
-open Environ
 open Util
 open Typeclasses_errors
 open Libobject
@@ -427,7 +426,6 @@ let add_class cl =
   cl.cl_projs
 
 
-open Declarations
       
 (*
  * interface functions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 4f88dd860d..585f066db4 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -10,7 +10,6 @@
 open Names
 open Term
 open Context
-open Evd
 open Environ
 open Constrexpr
 open Globnames
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index dd8087713f..7982fc8524 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -10,7 +10,6 @@ open Loc
 open Names
 open Term
 open Context
-open Evd
 open Environ
 open Constrexpr
 open Globnames
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index c933106d7c..1f822f1a58 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Environ
 open Evd