Removing dead code and unused opens.

77 files changed, 10 insertions, 292 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 2bd67dcdc..c5dfe3033 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -8,7 +8,6 @@
 
 open Errors
 open Util
-open Pp
 open Names
 open Term
 open Vars
diff --git a/engine/evd.ml b/engine/evd.ml
index b6849f7ff..b883db615 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -363,7 +363,6 @@ open Misctypes
 type t
 
 val empty : t
-val add_name_newly_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
 val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
 val remove_name_defined : Evar.t -> t -> t
 val rename : Evar.t -> Id.t -> t -> t
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 45b0aa231..cfca95d3e 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -32,7 +32,7 @@ struct
   let repr = ValT.repr
   let create = ValT.create
 
-  let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
+  let pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
 
   let typ_list = ValT.create "list"
   let typ_opt = ValT.create "option"
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 4b78bc05d..d67f1eee3 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -340,7 +340,6 @@ struct
   let lift = BackState.lift
   let once = BackState.once
   let break = BackState.break
-  let reflect = BackState.reflect
   let split = BackState.split
   let repr = BackState.repr
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ba664cafa..95e20bc25 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -925,8 +925,6 @@ end
 module UnsafeRepr = Proof.Unsafe
 
 let (>>=) = tclBIND
-let (<*>) = tclTHEN
-let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
 
 (** {6 Goal-dependent tactics} *)
 
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index aa1a75db6..6639b0201 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -44,12 +44,9 @@ module SentenceId : sig
   val mk_sentence :
     start:GText.mark -> stop:GText.mark -> flag list -> sentence
 
-  val set_flags : sentence -> flag list -> unit
   val add_flag : sentence -> flag -> unit
   val has_flag : sentence -> mem_flag -> bool
   val remove_flag : sentence -> mem_flag -> unit
-  val same_sentence : sentence -> sentence -> bool
-  val hidden_edit_id : unit -> int
   val find_all_tooltips : sentence -> int -> string list
   val add_tooltip : sentence -> int -> int -> string -> unit
   val set_index : sentence -> int -> unit
@@ -87,18 +84,15 @@ end = struct
     index = -1;
     changed_sig = new GUtil.signal ();
   }
-  let hidden_edit_id () = decr id; !id
 
   let changed s =
     s.changed_sig#call (s.index, List.map mem_flag_of_flag s.flags)
 
-  let set_flags s f = s.flags <- f; changed s
   let add_flag s f = s.flags <- CList.add_set (=) f s.flags; changed s
   let has_flag s mf =
     List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
   let remove_flag s mf =
     s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags; changed s
-  let same_sentence s1 s2 = s1.edit_id = s2.edit_id
   let find_all_tooltips s off =
     CList.map_filter (fun (start,stop,t) ->
       if start <= off && off <= stop then Some t else None)
diff --git a/ide/preferences.ml b/ide/preferences.ml
index addea9074..c4dc55972 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -386,14 +386,6 @@ let processing_color =
 let _ = attach_bg processing_color Tags.Script.to_process
 let _ = attach_bg processing_color Tags.Script.incomplete
 
-let default_tag = {
-  tag_fg_color = None;
-  tag_bg_color = None;
-  tag_bold = false;
-  tag_italic = false;
-  tag_underline = false;
-}
-
 let tags = ref Util.String.Map.empty
 
 let list_tags () = !tags
diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml
index 580f1fbcb..8f6cb382a 100644
--- a/ide/utils/okey.ml
+++ b/ide/utils/okey.ml
@@ -52,33 +52,6 @@ let int_of_modifier = function
   | `RELEASE -> 1 lsl 30
   | `SUPER -> 1 lsl 21
 
-let print_modifier l =
-  List.iter
-    (fun m ->
-      print_string
-	(((function
-	    `SHIFT -> "SHIFT"
-	  | `LOCK -> "LOCK"
-	  | `CONTROL -> "CONTROL"
-	  | `MOD1 -> "MOD1"
-	  | `MOD2 -> "MOD2"
-	  | `MOD3 -> "MOD3"
-	  | `MOD4 -> "MOD4"
-	  | `MOD5 -> "MOD5"
-	  | `BUTTON1 -> "B1"
-	  | `BUTTON2 -> "B2"
-	  | `BUTTON3 -> "B3"
-	  | `BUTTON4 -> "B4"
-	  | `BUTTON5 -> "B5"
-          | `HYPER -> "HYPER"                                                                                                     
-          | `META -> "META"                                                                                                       
-          | `RELEASE -> ""                                                                                                        
-          | `SUPER -> "SUPER")
-	    m)^" ")
-    )
-    l;
-  print_newline ()
-
 let int_of_modifiers l =
   List.fold_left (fun acc -> fun m -> acc + (int_of_modifier m)) 0 l
 
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 6c53fc013..aeae3e1fd 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -86,7 +86,7 @@ let signals = [
   end_s#disconnect;
 ] in
 object (self : 'a)
-  inherit GUtil.ml_signals signals as super
+  inherit GUtil.ml_signals signals
   method start_completion = start_s#connect ~after
   method update_completion = update_s#connect ~after
   method end_completion = end_s#connect ~after
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 4d95fdd0d..47c86045a 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -91,7 +91,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
       let () = proof#buffer#insert head_str in
       let () = insert_hyp hyps_hints hyps in
       let () =
-        let tags = Tags.Proof.goal :: if goal_hints <> [] then
+        let _ = if goal_hints <> [] then
           let tag = proof#buffer#create_tag [] in
           let () = hook_tag_cb tag goal_hints sel_cb on_hover in
           [tag]
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 83fbda487..218cedb36 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -287,7 +287,7 @@ let completion = new Wg_Completion.complete_model ct view#buffer in
 let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
 
 object (self)
-  inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super
+  inherit GSourceView2.source_view (Gobject.unsafe_cast tv)
 
   val undo_manager = new undo_manager view#buffer
 
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index b8f97e77c..011b31d9a 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -8,7 +8,6 @@
 
 open Loc
 open Tacexpr
-open Term
 open Misctypes
 open Genarg
 open Geninterp
@@ -49,9 +48,6 @@ let wit_quant_hyp = make0 "quant_hyp"
 let wit_constr =
   make0 "constr"
 
-let wit_constr_may_eval =
-  make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval"
-
 let wit_uconstr = make0 "uconstr"
 
 let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
@@ -60,9 +56,6 @@ let wit_constr_with_bindings = make0 "constr_with_bindings"
 
 let wit_bindings = make0 "bindings"
 
-let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
-  make0 "hyp_location_flag"
-
 let wit_red_expr = make0 "redexpr"
 
 let wit_clause_dft_concl  =
diff --git a/interp/notation.ml b/interp/notation.ml
index b8f4f3201..0a65dfc09 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -13,7 +13,6 @@ open Pp
 open Bigint
 open Names
 open Term
-open Nametab
 open Libnames
 open Globnames
 open Constrexpr
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index f9cf2691e..a705e3004 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -184,9 +184,6 @@ let rec pp_struct_const = function
 
 let pp_lbl lbl = str "L" ++ int lbl
 
-let pp_pcon (id,u) =
-  pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
-
 let pp_fv_elem = function
   | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
   | FVrel i -> str "Rel(" ++ int i ++ str ")"
diff --git a/kernel/names.ml b/kernel/names.ml
index 8e0237863..e8226d3d3 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -341,7 +341,7 @@ module ModPath = struct
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
       | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
-    let rec eq d1 d2 =
+    let eq d1 d2 =
       d1 == d2 ||
       match d1,d2 with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 7ac5b8d7b..4ed926f1f 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 open Errors
 open Names
-open Univ
 open Nativelib
 open Reduction
 open Util
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 0e56e76aa..c30789641 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,7 +15,6 @@
 
 open Util
 open Names
-open Univ
 open Term
 open Declarations
 open Context.Named.Declaration
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f23ed16f0..5bf369441 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -20,7 +20,6 @@ open Util
 open Names
 open Term
 open Vars
-open Univ
 open Environ
 open Closure
 open Esubst
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 4610dbcb0..89e833254 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -1,13 +1,9 @@
 open Util
 open Names
-open Term
 open Environ
-open Conv_oracle
 open Reduction
-open Closure
 open Vm
 open Csymtable
-open Univ
 
 let val_of_constr env c =
   val_of_constr (pre_env env) c
diff --git a/lib/spawn.ml b/lib/spawn.ml
index fda4b4239..2b9c4ccac 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -78,20 +78,6 @@ let accept (sr,sw) =
   set_binary_mode_out cout true;
   (csr, csw), cin, cout
 
-let handshake cin cout =
-  try
-    output_value cout (Hello (proto_version,Unix.getpid ())); flush cout;
-    match input_value cin with
-    | Hello(v, pid) when v = proto_version ->
-        prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
-        pid
-    | _ -> raise (Failure "handshake protocol")
-  with
-  | Failure s | Invalid_argument s | Sys_error s ->
-      pr_err ("Handshake failed: "  ^ s); raise (Failure "handshake")
-  | End_of_file ->
-      pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-
 let spawn_sock env prog args =
   let main_sock, main_sock_name = mk_socket_channel () in
   let extra = [| prog; "-main-channel"; main_sock_name |] in
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 6c02a7202..8b5f527cd 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -13,14 +13,9 @@ open Names
 open Locus
 open Misctypes
 open Genredexpr
-open Stdarg
 open Constrarg
 open Extraargs
-open Pcoq.Constr
-open Pcoq.Prim
-open Pcoq.Tactic
 
-open Proofview.Notations
 open Sigma.Notations
 
 DECLARE PLUGIN "coretactics"
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 79f80260f..1f3eb1335 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -14,13 +14,11 @@ open Stdarg
 open Constrarg
 open Extraargs
 open Pcoq.Prim
-open Pcoq.Constr
 open Pcoq.Tactic
 open Mod_subst
 open Names
 open Tacexpr
 open Glob_ops
-open Tactics
 open Errors
 open Util
 open Evd
@@ -128,7 +126,6 @@ TACTIC EXTEND ediscriminate
     [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-open Proofview.Notations
 let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
   discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
@@ -458,8 +455,6 @@ TACTIC EXTEND evar
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
-open Tacticals
-
 TACTIC EXTEND instantiate
   [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] ->
     [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ]
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 9ef154541..77075ec4c 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -10,8 +10,6 @@
 
 open Misctypes
 open Class_tactics
-open Pcoq.Prim
-open Pcoq.Constr
 open Pcoq.Tactic
 open Stdarg
 open Constrarg
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index df499a2c9..1bbdb1779 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -307,7 +307,6 @@ GEXTEND Gram
   ;
   END
 
-open Stdarg
 open Constrarg
 open Vernacexpr
 open Vernac_classifier
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index f2dbb5b6c..39db6268b 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -7,11 +7,9 @@
 (************************************************************************)
 
 open Util
-open Genarg
 open Pp
 open Names
 open Tacexpr
-open Geninterp
 
 (** Tactic notations (TacAlias) *)
 
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 977c56f38..3744449e9 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -475,9 +475,6 @@ let clause_app f = function
   | { onhyps=Some l; concl_occs=nl } ->
       { onhyps=Some(List.map f l); concl_occs=nl}
 
-let map_raw wit f ist x =
-  in_gen (glbwit wit) (f ist (out_gen (rawwit wit) x))
-
 (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
 let rec intern_atomic lf ist x =
   match (x:raw_atomic_tactic_expr) with
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 31bccd019..6a5d1380d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -21,7 +21,6 @@ open Libnames
 open Globnames
 open Nametab
 open Pfedit
-open Proof_type
 open Refiner
 open Tacmach.New
 open Tactic_debug
@@ -35,8 +34,6 @@ open Stdarg
 open Constrarg
 open Printer
 open Pretyping
-module Monad_ = Monad
-open Evd
 open Misctypes
 open Locus
 open Tacintern
@@ -196,7 +193,7 @@ module Value = struct
   | OptArg t -> Val.Opt (tag_of_arg t)
   | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
 
-  let rec val_cast arg v = prj (tag_of_arg arg) v
+  let val_cast arg v = prj (tag_of_arg arg) v
 
   let cast (Topwit wit) v = val_cast wit v
 
@@ -695,13 +692,6 @@ let pf_interp_casted_constr ist gl c =
 let pf_interp_constr ist gl =
   interp_constr ist (pf_env gl) (project gl)
 
-let new_interp_constr ist c k =
-  let open Proofview in
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
-    let (sigma, c) = interp_constr ist (Goal.env gl) (project gl) c in
-    Sigma.Unsafe.of_pair (k c, sigma)
-  end }
-
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
     try match dest_fun x with
@@ -1290,7 +1280,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
   | TacML (loc,opn,l) ->
-      let open Ftactic.Notations in
       let trace = push_trace (loc,LtacMLCall tac) ist in
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       let tac = Tacenv.interp_ml_tactic opn in
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 54d32f266..1326818fc 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -16,7 +16,6 @@ open Globnames
 open Term
 open Genredexpr
 open Patternops
-open Pretyping
 
 (** Substitution of tactics at module closing time *)
 
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index 7cda8d914..655bfd5f5 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -10,17 +10,12 @@ open Term
 open Hipattern
 open Names
 open Pp
-open Genarg
 open Geninterp
-open Stdarg
 open Misctypes
 open Tacexpr
 open Tacinterp
-open Tactics
-open Errors
 open Util
 open Tacticals.New
-open Proofview.Notations
 
 let tauto_plugin = "tauto"
 let () = Mltop.add_known_module tauto_plugin
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index f0c12ab8e..04b622864 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -14,9 +14,7 @@ open Extend
 open Constrexpr
 open Notation_term
 open Libnames
-open Tacexpr
 open Names
-open Egramml
 
 (**************************************************************************)
 (*
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 37fccdb3c..95ac87247 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Util
-open Compat
-open Names
 open Extend
 open Pcoq
 open Genarg
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 1c39858ea..35ba9757d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -20,7 +20,6 @@ open Misctypes
 open Tok (* necessary for camlp4 *)
 
 open Pcoq
-open Pcoq.Tactic
 open Pcoq.Prim
 open Pcoq.Constr
 open Pcoq.Vernac_
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 53d2089c0..fe9ab630f 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -12,7 +12,6 @@ open Errors
 open Util
 open Extend
 open Genarg
-open Tok (* necessary for camlp4 *)
 
 (** The parser of Coq *)
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index c01214377..898dcd255 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -154,11 +154,6 @@ let rec term_equal t1 t2 =
 
 open Hashset.Combine
 
-let hash_sorts_family = function
-| InProp -> 0
-| InSet -> 1
-| InType -> 2
-
 let rec hash_term = function
   | Symb c -> combine 1 (hash_constr c)
   | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 9a53e2e16..52a135119 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -11,8 +11,6 @@
 open Cctac
 open Stdarg
 open Constrarg
-open Pcoq.Prim
-open Pcoq.Constr
 
 DECLARE PLUGIN "cc_plugin"
 
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 802c36109..78a95143d 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Util
 open Compat
 open Pp
 open Decl_expr
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 35a5a7616..39cad4d03 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Constrarg
-open Pcoq.Prim
-open Pcoq.Constr
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 41a068ff3..67c1c5901 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -19,7 +19,6 @@ open Table
 open Extraction
 open Modutil
 open Common
-open Mod_subst
 
 (***************************************)
 (*S Part I: computing Coq environment. *)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index ca4e13e12..eb2f02244 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -14,7 +14,6 @@ open Genarg
 open Stdarg
 open Constrarg
 open Pcoq.Prim
-open Pcoq.Constr
 open Pp
 open Names
 open Nameops
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index df79c585e..8874afef3 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,8 +1,6 @@
 open Pp
-open Errors
 open Util
 open Names
-open Nameops
 open Globnames
 open Table
 open Miniml
@@ -18,9 +16,6 @@ let json_int i =
 let json_bool b =
   if b then str "true" else str "false"
 
-let json_null =
-  str "null"
-
 let json_global typ ref =
   json_str (Common.pp_global typ ref)
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b5e8b4804..bd4831130 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -380,14 +380,6 @@ let rec depcheck_struct = function
       let lse' = depcheck_se lse in
       if List.is_empty lse' then struc' else (mp,lse')::struc'
 
-let is_prefix pre s =
-  let len = String.length pre in
-  let rec is_prefix_aux i =
-    if Int.equal i len then true
-    else pre.[i] == s.[i] && is_prefix_aux (succ i)
-  in
-  is_prefix_aux 0
-
 exception RemainingImplicit of kill_reason
 
 let check_for_remaining_implicits struc =
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index b04c4a50c..134b6ba94 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -18,7 +18,6 @@ open Libnames
 open Constrarg
 open Stdarg
 open Pcoq.Prim
-open Pcoq.Tactic
 
 DECLARE PLUGIN "ground_plugin"
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 0bc40136c..0e2a40245 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -12,7 +12,6 @@ open Errors
 open Util
 open Term
 open Vars
-open Glob_term
 open Tacmach
 open Tactics
 open Tacticals
@@ -98,8 +97,6 @@ let rec collect_quantified seq=
 
 (* open instances processor *)
 
-let dummy_constr=mkMeta (-1)
-
 let dummy_bvid=Id.of_string "x"
 
 let mk_open_instance id idc gl m t=
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 8bc84608e..dc5dd45ab 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -16,7 +16,6 @@ open Term
 open Tactics
 open Names
 open Globnames
-open Tacmach
 open Fourier
 open Contradiction
 open Proofview.Notations
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 02cd819f4..839586528 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -5,7 +5,6 @@ open Term
 open Vars
 open Namegen
 open Names
-open Declarations
 open Pp
 open Tacmach
 open Termops
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0ba18f568..6dfc23511 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -9,15 +9,12 @@
 open Compat
 open Util
 open Term
-open Vars
-open Names
 open Pp
 open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
 open Constrarg
-open Tacticals
 open Misctypes
 open Pcoq.Prim
 open Pcoq.Constr
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 046c7aa43..e98ac5fb5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -208,7 +208,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob
 (* Debugging mechanism *)
 let debug_queue = Stack.create ()
 
-let rec print_debug_queue b e = 
+let print_debug_queue b e = 
   if  not (Stack.is_empty debug_queue) 
   then
     begin
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5fef6d3fc..5c0a8226a 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -18,9 +18,7 @@
 
 open Pp
 open Mutils
-open Proofview
 open Goptions
-open Proofview.Notations
 
 (**
   * Debug flag 
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index bca1c2feb..e6b5cc60d 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,12 +16,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Errors
-open Misctypes
-open Stdarg
 open Constrarg
-open Pcoq.Prim
-open Pcoq.Tactic
 
 DECLARE PLUGIN "micromega_plugin"
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index b314e0d85..d7538146f 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -20,7 +20,6 @@ DECLARE PLUGIN "omega_plugin"
 open Names
 open Coq_omega
 open Constrarg
-open Pcoq.Prim
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e4c8da93b..fd87d5b7d 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -14,9 +14,6 @@ open Tacexpr
 open Geninterp
 open Quote
 open Constrarg
-open Pcoq.Prim
-open Pcoq.Constr
-open Pcoq.Tactic
 
 DECLARE PLUGIN "quote_plugin"
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 61efa9f54..fd4ede6c3 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -13,7 +13,6 @@ DECLARE PLUGIN "romega_plugin"
 open Names
 open Refl_omega
 open Constrarg
-open Pcoq.Prim
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 1ebb6e6b7..f5a734048 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -16,7 +16,6 @@ open Newring_ast
 open Newring
 open Stdarg
 open Constrarg
-open Pcoq.Prim
 open Pcoq.Constr
 open Pcoq.Tactic
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 7ef89b7a0..271bf35a8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,11 +153,6 @@ let ic_unsafe c = (*FIXME remove *)
   let sigma = Evd.from_env env in
     fst (Constrintern.interp_constr env sigma c)
 
-let ty c =
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-    Typing.unsafe_type_of env sigma c
-
 let decl_constant na ctx c =
   let vars = Universes.universes_of_constr c in
   let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
@@ -185,9 +180,6 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
   let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
   Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
 
-let ltac_record flds =
-  TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
-
 let dummy_goal env sigma =
   let (gl,_,sigma) = 
     Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in
@@ -290,8 +282,6 @@ let my_reference c =
 
 let new_ring_path =
   DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
-let ltac s =
-  lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s))
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
@@ -318,21 +308,12 @@ let coq_mk_reqe = my_constant "mk_reqe"
 let coq_semi_ring_theory = my_constant "semi_ring_theory"
 let coq_mk_seqe = my_constant "mk_seqe"
 
-let ltac_inv_morph_gen = zltac"inv_gen_phi"
-let ltac_inv_morphZ = zltac"inv_gen_phiZ"
-let ltac_inv_morphN = zltac"inv_gen_phiN"
-let ltac_inv_morphNword = zltac"inv_gen_phiNword"
 let coq_abstract = my_constant"Abstract"
 let coq_comp = my_constant"Computational"
 let coq_morph = my_constant"Morphism"
 
-(* morphism *)
-let coq_ring_morph = my_constant "ring_morph"
-let coq_semi_morph = my_constant "semi_morph"
-
 (* power function *)
 let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
-let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
 
 (* hypothesis *)
 let coq_mkhypo = my_reference "mkhypo"
@@ -583,18 +564,6 @@ let dest_ring env sigma th_spec =
     | _ -> error "bad ring structure"
 
 
-let dest_morph env sigma m_spec =
-  let m_typ = Retyping.get_type_of env sigma m_spec in
-  match kind_of_term m_typ with
-      App(f,[|r;zero;one;add;mul;sub;opp;req;
-              c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-        when eq_constr_nounivs f (Lazy.force coq_ring_morph) ->
-          (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
-    | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when eq_constr_nounivs f (Lazy.force coq_semi_morph) ->
-        (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
-    | _ -> error "bad morphism structure"
-
 let reflect_coeff rkind =
   (* We build an ill-typed terms on purpose... *)
   match rkind with
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index ef3a3f525..d349cf821 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Pp
 open Names
@@ -14,7 +13,6 @@ open Term
 open Vars
 open Termops
 open Namegen
-open Pre_env
 open Environ
 open Evd
 open Evarutil
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3d1822102..455a7dbd6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -20,7 +20,6 @@ open Reductionops
 open Evarutil
 open Pretype_errors
 open Sigma.Notations
-open Context.Rel.Declaration
 
 let normalize_evar evd ev =
   match kind_of_term (whd_evar evd (mkEvar ev)) with
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 8ddfeaf2f..17bf28793 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -18,7 +18,6 @@ open Inductive
 open Util
 open Nativecode
 open Nativevalues
-open Nativelambda
 open Context.Rel.Declaration
 
 (** This module implements normalization by evaluation to OCaml code *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3a5796fe1..3ff96cd72 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -25,7 +25,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
 
 open Goptions
 
-let set_typeclasses_unique_solutions =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f0548238a..10b2bda05 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -99,11 +99,6 @@ module Make
     | ETBinder false -> str "closed binder"
     | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
 
-  let strip_meta id =
-    let s = Id.to_string id in
-    if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
-    else id
-
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
     | CommentString s -> qs s
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 9354cd28d..5f98eeeab 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -65,7 +65,6 @@ let get_new_id locals id =
 
 (** Inductive declarations *)
 
-open Termops
 open Reduction
 
 let print_params env sigma params =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index db0b26f7e..76e2d7dc5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
-open Proofview_monad
 open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
diff --git a/stm/spawned.ml b/stm/spawned.ml
index c6df87267..2eae6f5e2 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -13,19 +13,6 @@ let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
 
 type chandescr = AnonPipe | Socket of string * int * int
 
-let handshake cin cout =
-  try
-    match input_value cin with
-    | Hello(v, pid) when v = proto_version ->
-        prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
-        output_value cout (Hello (proto_version,Unix.getpid ())); flush cout
-    | _ -> raise (Failure "handshake protocol")
-  with
-  | Failure s | Invalid_argument s | Sys_error s ->
-      pr_err ("Handshake failed: "  ^ s); raise (Failure "handshake")
-  | End_of_file ->
-      pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-
 let open_bin_connection h pr pw =
   let open Unix in
   let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
diff --git a/stm/stm.ml b/stm/stm.ml
index c296361a1..b6ba5815a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1343,7 +1343,6 @@ end = struct (* {{{ *)
   let set_perspective idl =
     ProofTask.set_perspective idl;
     TaskQueue.broadcast (Option.get !queue);
-    let open Stateid in
     let open ProofTask in
     let overlap s1 s2 =
       List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 950eeef52..6d6e51536 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -15,10 +15,8 @@ open Term
 open Termops
 open Errors
 open Util
-open Tacexpr
 open Mod_subst
 open Locus
-open Sigma.Notations
 open Proofview.Notations
 
 (* Rewriting rules *)
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index ab6fb37fd..26166bd83 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -6,14 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Term
 open Hipattern
 open Tactics
 open Coqlib
 open Reductionops
 open Misctypes
-open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 9cfb805d4..6bbd9b2e8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -17,12 +17,10 @@ open Proof_type
 open Tacticals
 open Tacmach
 open Tactics
-open Patternops
 open Clenv
 open Auto
 open Genredexpr
 open Tacexpr
-open Misctypes
 open Locus
 open Locusops
 open Hints
@@ -52,16 +50,6 @@ let registered_e_assumption =
               (Tacmach.New.pf_ids_of_hyps gl))
   end }
 
-let eval_uconstrs ist cs =
-  let flags = {
-    Pretyping.use_typeclasses = false;
-    use_unif_heuristics = true;
-    use_hook = Some Pfedit.solve_by_implicit_tactic;
-    fail_evar = false;
-    expand_evars = true
-  } in
-  List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
-
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
@@ -114,7 +102,6 @@ let prolog_tac l n =
   end
 
 open Auto
-open Unification
 
 (***************************************************************************)
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 011296a8d..ef361d326 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -12,7 +12,6 @@
 (*                           by Eduardo Gimenez                        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Names
 open Namegen
@@ -27,7 +26,6 @@ open Hipattern
 open Pretyping
 open Tacmach.New
 open Coqlib
-open Proofview.Notations
 
 (* This file containts the implementation of the tactics ``Decide
    Equality'' and ``Compare''. They can be used to decide the
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0bb842601..2fe4d620e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4652,7 +4652,6 @@ let rec shrink ctx sign c t accu =
 | _ -> assert false
 
 let shrink_entry sign const =
-  let open Context.Named.Declaration in
   let open Entries in
   let typ = match const.const_entry_type with
   | None -> assert false
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 431080c6b..81c01f29d 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -75,7 +75,7 @@
     let stop_env () = if !r then stop (); r := false in
       (fun x -> !r), start_env, stop_env
       
-  let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+  let _, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
   let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
 
   let url_buffer = Buffer.create 40
@@ -111,12 +111,6 @@
     Cdglobals.gallina := s.st_gallina;
     Cdglobals.light := s.st_light
 
-  let without_ref r f x = save_state (); r := false; f x; restore_state ()
-
-  let without_gallina = without_ref Cdglobals.gallina
-
-  let without_light = without_ref Cdglobals.light
-
   let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
   let end_show () = restore_state ()
 
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 47acc7b43..9be791a8d 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -77,32 +77,6 @@ let find m l = Hashtbl.find reftable (m, l)
 
 let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
-(*s Manipulating path prefixes *)
-
-type stack = string list
-
-let rec string_of_stack st =
-  match st with
-    | [] -> ""
-    | x::[] -> x
-    | x::tl -> (string_of_stack tl) ^ "." ^ x
-
-let empty_stack = []
-
-let module_stack = ref empty_stack
-let section_stack = ref empty_stack
-
-let push st p = st := p::!st
-let pop st =
-  match !st with
-    | [] -> ()
-    | _::tl -> st := tl
-
-let head st =
-  match st with
-    | [] -> ""
-    | x::_ -> x
-
 (* Coq modules *)
 
 let split_sp s =
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2b2690968..82d3d62b5 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -953,7 +953,7 @@ module TeXmacs = struct
 
   (*s Latex preamble *)
 
-  let (preamble : string Queue.t) =
+  let (_ : string Queue.t) =
     in_doc := false; Queue.create ()
 
   let header () =
@@ -1122,7 +1122,6 @@ module Raw = struct
     for i = 0 to String.length s - 1 do char s.[i] done
 
   let start_module () = ()
-  let end_module () = ()
 
   let start_latex_math () = ()
   let stop_latex_math () = ()
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 38bc0e568..5865fec06 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -13,7 +13,6 @@ open Flags
 open Term
 open Vars
 open Termops
-open Entries
 open Environ
 open Redexpr
 open Declare
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 04182cf23..c6f49dcd4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -9,7 +9,6 @@
 open Pp
 open Errors
 open Util
-open System
 open Flags
 open Names
 open Libnames
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index ffa11679c..6b267283a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -11,7 +11,6 @@ open Errors
 open Util
 open Term
 open Vars
-open Entries
 open Declarations
 open Cooking
 open Entries
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a041ee620..701bc5da5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -23,7 +23,6 @@ open Vernacexpr
 open Pcoq
 open Libnames
 open Tok
-open Egramml
 open Egramcoq
 open Notation
 open Nameops
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 93429da5a..d12b5ee8e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -26,7 +26,6 @@ open Constrexpr_ops
 open Goptions
 open Sigma.Notations
 open Context.Rel.Declaration
-open Entries
 
 (********** definition d'un record (structure) **************)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 89bc31d0a..1c8d60251 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -12,7 +12,6 @@ open Pp
 open Errors
 open Util
 open Flags
-open System
 open Vernacexpr
 
 (* The functions in this module may raise (unexplainable!) exceptions.