Merge PR#582: Fix warnings

7 files changed, 3 insertions, 16 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf3..3f99a3c7c0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args =
       | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
          GApp (loc, GRef (loc', ref, us), arg)
       | Some _, _ ->
-        user_err ~loc  (str "Notation " ++ pr_qualid qid ++
-          str " cannot have a universe instance, its expanded head
-               does not start with a reference")
+        user_err ~loc  (str "Notation " ++ pr_qualid qid
+                        ++ str " cannot have a universe instance,"
+                        ++ str " its expanded head does not start with a reference")
       in
       c, projapp, args2
 
@@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t =
   let t' = locate_if_hole (loc_of_glob_constr t) na t in
   understand_tcc_evars env evdref ~expected_type:IsType t'
 
-open Environ
-
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 758d4e650b..fdd50c6a1e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -18,7 +18,6 @@ open Constrexpr
 open Notation_term
 open Pretyping
 open Misctypes
-open Decl_kinds
 
 (** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 90ac7f7296..6aa6f54c05 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -22,7 +22,6 @@ open Glob_ops
 open Ppextend
 open Context.Named.Declaration
 
-module NamedDecl = Context.Named.Declaration
 (*i*)
 
 (*s A scope is a set of notations; it includes
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8b4fadb5a0..d08fb107be 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1141,10 +1141,6 @@ let term_of_binder = function
   | Name id -> GVar (Loc.ghost,id)
   | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
-type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
-      glob_constr option * glob_constr
-
 let match_notation_constr u c (metas,pat) =
   let terms,binders,termlists,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 341ff5662c..5920b0d508 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Misctypes
-open Tactypes
 open Genarg
 open Geninterp
 
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 113fe40ba7..ac40a23281 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -10,7 +10,6 @@
 
 open Loc
 open Names
-open Term
 open EConstr
 open Libnames
 open Globnames
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index c3f4c4f302..ed7b0b70d4 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -106,5 +106,3 @@ let search_syntactic_definition kn =
   let def = out_pat pat in
   verbose_compat kn def v;
   def
-
-open Goptions