aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-08 18:59:55 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-08 19:59:03 +0200
commitf461e7657cab9917c5b405427ddba3d56f197efb (patch)
tree467ac699f78d0360b05174238aeb1177da892503
parent9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff)
Removing dead code and unused opens.
-rw-r--r--engine/evarutil.ml1
-rw-r--r--engine/evd.ml1
-rw-r--r--engine/geninterp.ml2
-rw-r--r--engine/logic_monad.ml1
-rw-r--r--engine/proofview.ml2
-rw-r--r--ide/coqOps.ml6
-rw-r--r--ide/preferences.ml8
-rw-r--r--ide/utils/okey.ml27
-rw-r--r--ide/wg_Completion.ml2
-rw-r--r--ide/wg_ProofView.ml2
-rw-r--r--ide/wg_ScriptView.ml2
-rw-r--r--interp/constrarg.ml7
-rw-r--r--interp/notation.ml1
-rw-r--r--kernel/cbytecodes.ml3
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/nativeconv.ml1
-rw-r--r--kernel/pre_env.ml1
-rw-r--r--kernel/reduction.ml1
-rw-r--r--kernel/vconv.ml4
-rw-r--r--lib/spawn.ml14
-rw-r--r--ltac/coretactics.ml45
-rw-r--r--ltac/extratactics.ml45
-rw-r--r--ltac/g_class.ml42
-rw-r--r--ltac/g_ltac.ml41
-rw-r--r--ltac/tacenv.ml2
-rw-r--r--ltac/tacintern.ml3
-rw-r--r--ltac/tacinterp.ml13
-rw-r--r--ltac/tacsubst.ml1
-rw-r--r--ltac/tauto.ml5
-rw-r--r--parsing/egramcoq.ml2
-rw-r--r--parsing/egramml.ml2
-rw-r--r--parsing/g_vernac.ml41
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--plugins/cc/ccalgo.ml5
-rw-r--r--plugins/cc/g_congruence.ml42
-rw-r--r--plugins/decl_mode/g_decl_mode.ml41
-rw-r--r--plugins/derive/g_derive.ml42
-rw-r--r--plugins/extraction/extract_env.ml1
-rw-r--r--plugins/extraction/g_extraction.ml41
-rw-r--r--plugins/extraction/json.ml5
-rw-r--r--plugins/extraction/modutil.ml8
-rw-r--r--plugins/firstorder/g_ground.ml41
-rw-r--r--plugins/firstorder/instances.ml3
-rw-r--r--plugins/fourier/fourierR.ml1
-rw-r--r--plugins/funind/functional_principles_proofs.ml1
-rw-r--r--plugins/funind/g_indfun.ml43
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/micromega/coq_micromega.ml2
-rw-r--r--plugins/micromega/g_micromega.ml45
-rw-r--r--plugins/omega/g_omega.ml41
-rw-r--r--plugins/quote/g_quote.ml43
-rw-r--r--plugins/romega/g_romega.ml41
-rw-r--r--plugins/setoid_ring/g_newring.ml41
-rw-r--r--plugins/setoid_ring/newring.ml31
-rw-r--r--pretyping/evardefine.ml2
-rw-r--r--pretyping/evarsolve.ml1
-rw-r--r--pretyping/nativenorm.ml1
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--printing/ppvernac.ml5
-rw-r--r--printing/printmod.ml1
-rw-r--r--proofs/refine.ml2
-rw-r--r--stm/spawned.ml13
-rw-r--r--stm/stm.ml1
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/contradiction.ml2
-rw-r--r--tactics/eauto.ml13
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/tactics.ml1
-rw-r--r--tools/coqdoc/cpretty.mll8
-rw-r--r--tools/coqdoc/index.ml26
-rw-r--r--tools/coqdoc/output.ml3
-rw-r--r--toplevel/command.ml1
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/discharge.ml1
-rw-r--r--toplevel/metasyntax.ml1
-rw-r--r--toplevel/record.ml1
-rw-r--r--toplevel/vernac.ml1
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.