Remove some more "open" and dead code thanks to OCaml4 warnings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7

45 files changed, 9 insertions, 469 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 40599b827..89e30a8ee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -58,8 +58,6 @@ module ST=struct
 
   let query sign st=Hashtbl.find st.toterm sign
 
-  let rev_query term st=Hashtbl.find st.tosign term
-
   let delete st t=
     try let sign=Hashtbl.find st.tosign t in
 	Hashtbl.remove st.toterm sign;
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index d5eab32c4..25c01f2bd 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,7 +10,6 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open Errors
-open Util
 open Names
 open Term
 open Ccalgo
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 78273dabc..c2c437c80 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -9,8 +9,6 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Cctac
-open Tactics
-open Tacticals
 
 (* Tactic registration *)
 
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index f29964c69..1f55257e5 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -12,7 +12,6 @@ open Evd
 open Errors
 open Util
 
-
 let daimon_flag = ref false
 
 let set_daimon_flag () = daimon_flag:=true
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 1a0d05047..367e02bf8 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -11,7 +11,6 @@ open Util
 open Pp
 open Evd
 
-open Proof_type
 open Tacmach
 open Tacinterp
 open Decl_expr
@@ -129,22 +128,6 @@ let daimon_tac gls =
   set_daimon_flag ();
   {it=[];sigma=sig_sig gls}
 
-
-(* marking closed blocks *)
-
-let rec is_focussing_instr = function
-    Pthus i | Pthen i | Phence i -> is_focussing_instr i
-  | Pescape | Pper _ | Pclaim _ | Pfocus _
-  | Psuppose _ | Pcase (_,_,_)  -> true
-  | _ -> false
-
-let mark_rule_as_done = function
-    Decl_proof true -> Decl_proof false
-  | Decl_proof false ->
-      anomaly "already marked as done"
-  | _ -> anomaly "mark_rule_as_done"
-
-
 (* post-instruction focus management *)
 
 (* spiwack: This used to fail if there was no focusing command
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 3eaf81d2b..e8e81c472 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -14,13 +14,10 @@ open Pp
 open Tok
 open Decl_expr
 open Names
-open Term
-open Genarg
 open Pcoq
 
 open Pcoq.Constr
 open Pcoq.Tactic
-open Pcoq.Vernac_
 
 let pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index b72476a75..01f32e4a3 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Pp
 open Decl_expr
 open Names
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2baea11a3..f49b1f375 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -70,16 +70,12 @@ module type VISIT = sig
   (* Reset the dependencies by emptying the visit lists *)
   val reset : unit -> unit
 
-  (* Add the module_path and all its prefixes to the mp visit list *)
-  val add_mp : module_path -> unit
-
-  (* Same, but we'll keep all fields of these modules *)
+  (* Add the module_path and all its prefixes to the mp visit list.
+     We'll keep all fields of these modules. *)
   val add_mp_all : module_path -> unit
 
-  (* Add kernel_name / constant / reference / ... in the visit lists.
+  (* Add reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
-  val add_ind : mutual_inductive -> unit
-  val add_con : constant -> unit
   val add_ref : global_reference -> unit
   val add_decl_deps : ml_decl -> unit
   val add_spec_deps : ml_spec -> unit
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 58e9a5220..bdb102b18 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -10,8 +10,6 @@
 
 (* ML names *)
 
-open Vernacexpr
-open Pcoq
 open Genarg
 open Pp
 open Names
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 4fd9f17ee..33da06f01 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -13,7 +13,6 @@ open Errors
 open Util
 open Names
 open Nameops
-open Libnames
 open Globnames
 open Table
 open Miniml
@@ -82,10 +81,6 @@ let pp_global k r =
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let kn_sig =
-  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
-  make_mind specif empty_dirpath (mk_label "sig")
-
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index e3abab82b..b53fec23e 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -224,21 +224,6 @@ let type_maxvar t =
     | _ -> n
   in parse 0 t
 
-(*s What are the type variables occurring in [t]. *)
-
-let intset_union_map_list f l =
-  List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
-
-let intset_union_map_array f a =
-  Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
-
-let rec type_listvar = function
-  | Tmeta {contents = Some t} -> type_listvar t
-  | Tvar i | Tvar' i -> Intset.singleton i
-  | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
-  | Tglob (_,l) -> intset_union_map_list type_listvar l
-  | _ -> Intset.empty
-
 (*s From [a -> b -> c] to [[a;b],c]. *)
 
 let rec type_decomp = function
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9247baba2..4a390128a 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -289,8 +289,6 @@ and optim_me to_appear s = function
    For non-library extraction, we recompute a minimal set of dependencies
    for first-level objects *)
 
-exception NoDepCheck
-
 let base_r = function
   | ConstRef c as r -> r
   | IndRef (kn,_) -> IndRef (kn,0)
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 59a820bc0..303932484 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -12,11 +12,8 @@ open Formula
 open Sequent
 open Ground
 open Goptions
-open Tactics
 open Tacticals
 open Tacinterp
-open Term
-open Names
 open Libnames
 
 (* declaring search depth as a global option *)
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index c648939bb..238813e39 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -48,8 +48,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 		| LLexists (_,_)   ->  50
 		| LLarrow  (_,_,_) -> -10
 
-let left_reversible lpat=(priority lpat)>0
-
 module OrderedFormula=
 struct
   type t=Formula.t
@@ -163,8 +161,6 @@ let find_left t seq=List.hd (CM.find t seq.context)
       left_reversible lpat
   with Heap.EmptyHeap -> false
 *)
-let no_formula seq=
-  seq.redexes=HP.empty
 
 let rec take_formula seq=
   let hd=HP.maximum seq.redexes
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index b45932e57..429a0a4a8 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -14,7 +14,6 @@ des inéquations et équations sont entiers. En attendant la tactique Field.
 
 open Term
 open Tactics
-open Clenv
 open Names
 open Libnames
 open Globnames
@@ -76,7 +75,6 @@ let flin_emult a f =
 ;;
 
 (*****************************************************************************)
-open Vernacexpr
 
 type ineq = Rlt | Rle | Rgt | Rge
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3505c4d9b..52b4d881a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -134,19 +134,6 @@ let refine c =
 let thin l =
   Tacmach.thin_no_check l
 
-
-let cut_replacing id t tac :tactic=
-  tclTHENS (cut t)
-    [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
-      tac
-    ]
-
-let intro_erasing id = tclTHEN (thin [id]) (introduction id)
-
-
-
-let rec_hyp_id = id_of_string "rec_hyp"
-
 let is_trivial_eq t =
   let res =   try
     begin
@@ -367,7 +354,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
     new_ctxt,new_end_of_type,simpl_eq_tac
 
 
-let is_property ptes_info t_x full_type_of_hyp =
+let is_property (ptes_info:ptes_info) t_x full_type_of_hyp =
   if isApp t_x
   then
     let pte,args = destApp t_x in
@@ -563,7 +550,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
     thin [hyp_id],[]
 
 
-let clean_goal_with_heq ptes_infos continue_tac dyn_infos  =
+let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) =
   fun g ->
     let env = pf_env g
     and sigma = project g
@@ -894,13 +881,6 @@ let build_proof
 
 
 (* Proof of principles from structural functions *)
-let is_pte_type t =
-  isSort ((strip_prod t))
-
-let is_pte (_,_,t) = is_pte_type t
-
-
-
 
 type static_fix_info =
     {
@@ -932,9 +912,6 @@ let prove_rec_hyp fix_info  =
     is_valid = fun _ -> true
   }
 
-
-exception Not_Rec
-
 let generalize_non_dep hyp g =
 (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
   let hyps = [hyp] in
@@ -1427,17 +1404,6 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
     backtrack gls
 
 
-
-let build_clause eqs =
-  {
-    Locus.onhyps =
-      Some (List.map
-	      (fun id -> (Locus.AllOccurrences, id), Locus.InHyp)
-	      eqs
-	   );
-    Locus.concl_occs = Locus.NoOccurrences
-  }
-
 let rec rewrite_eqs_in_eqs eqs =
   match eqs with
     | [] -> tclIDTAC
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b97fc48f1..a14b47393 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -289,22 +289,6 @@ let change_property_sort toSort princ princName =
 let pp_dur time time' =
   str (string_of_float (System.time_difference time time'))
 
-(* let qed () = save_named true  *)
-let defined () =
-  try
-    Lemmas.save_named false
-  with
-    | UserError("extract_proof",msg) ->
-	Errors.errorlabstrm
-	  "defined"
-	  ((try
-	      str "On goal : " ++ fnl () ++  pr_open_subgoals () ++ fnl ()
-	    with _ -> mt ()
-	   ) ++msg)
-    | e -> raise e
-
-
-
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index dccbfa3b5..77c6dc493 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -14,9 +14,7 @@ open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
-open Pcoq
 open Tacticals
-open Constr
 open Misctypes
 open Miscops
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b820489f5..61390bb1a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -288,10 +288,6 @@ let make_discr_match brl =
 	   make_discr_match_el el,
 	   make_discr_match_brl i brl)
 
-let pr_name = function
-  | Name id -> Ppconstr.pr_id id
-  | Anonymous -> str "_"
-
 (**********************************************************************)
 (*  functions used to build case expression from lettuple and if ones *)
 (**********************************************************************)
@@ -326,40 +322,6 @@ let build_constructors_of_type ind' argl =
 	     )
     ind.Declarations.mind_consnames
 
-(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
-let rec find_type_of nb b =
-  let f,_ = glob_decompose_app b in
-  match f with
-    | GRef(_,ref) ->
-	begin
-	  let ind_type  =
-	    match ref with
-	      | VarRef _ | ConstRef _ ->
-		  let constr_of_ref = constr_of_global ref in
-		  let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in
-		  let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in
-		  let ret_type,_ = decompose_app ret_type in
-		  if not (isInd ret_type) then
-		    begin
-(* 		      Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *)
-		      raise (Invalid_argument "not an inductive")
-		    end;
-		  destInd ret_type
-	      | IndRef ind -> ind
-	      | ConstructRef c -> fst c
-	  in
-	  let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in
-	  if not (Array.length ind_type_info.Declarations.mind_consnames = nb )
-	  then raise (Invalid_argument "find_type_of : not a valid inductive");
-	  ind_type
-	end
-    | GCast(_,b,_) -> find_type_of nb b
-    | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *)
-    | _ -> raise (Invalid_argument "not a ref")
-
-
-
-
 (******************)
 (* Main functions *)
 (******************)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index edc727a48..48ed14473 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -21,7 +21,7 @@ let is_rec_info scheme_info =
       Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
   in
-  Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+  List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
 
 let choose_dest_or_ind scheme_info =
     if is_rec_info scheme_info
@@ -496,64 +496,6 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 let map_option f = function 
   | None -> None 
   | Some v -> Some (f v)
-    
-let decompose_lambda_n_assum_constr_expr = 
-  let rec decompose_lambda_n_assum_constr_expr acc n e = 
-  if n = 0 then (List.rev acc,e)
-  else
-    match e with 
-      | Constrexpr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e'
-      | Constrexpr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
-	let nal_length = List.length nal in 
-	if nal_length <= n 
-	then
-	  decompose_lambda_n_assum_constr_expr 
-	    (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
-	    (n - nal_length) 
-	    (Constrexpr.CLambdaN(lambda_loc,bl,e'))
-  	else
-	  let nal_keep,nal_expr = List.chop n nal in 
-	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
-	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
-	  )
-      | Constrexpr.CLetIn(_, na,nav,e') ->
-	decompose_lambda_n_assum_constr_expr 
-	  (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
-      | _ -> error "Not enough product or assumption"
-  in
-  decompose_lambda_n_assum_constr_expr []
-
-let decompose_prod_n_assum_constr_expr = 
-  let rec decompose_prod_n_assum_constr_expr acc n e = 
-    (* Pp.msgnl (str "n := " ++ int n ++ fnl ()++ *)
-    (* 		str "e := " ++ Ppconstr.pr_lconstr_expr e); *)
-  if n = 0 then 
-    (* let _ = Pp.msgnl (str "return_type := " ++ Ppconstr.pr_lconstr_expr e) in  *)
-      (List.rev acc,e)
-  else
-    match e with 
-      | Constrexpr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e'
-      | Constrexpr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
-	let nal_length = List.length nal in 
-	if nal_length <= n 
-	then
-	  (* let _ = Pp.msgnl (str "first case") in  *)
-	  decompose_prod_n_assum_constr_expr 
-	    (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
-	    (n - nal_length) 
-	    (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e')))
-  	else
-	  (* let _ = Pp.msgnl (str "second case") in  *)
-	  let nal_keep,nal_expr = List.chop n nal in 
-	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
-	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
-	  )
-      | Constrexpr.CLetIn(_, na,nav,e') ->
-	decompose_prod_n_assum_constr_expr 
-	  (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
-      | _ -> error "Not enough product or assumption"
-  in
-  decompose_prod_n_assum_constr_expr []
 
 open Constrexpr
 open Topconstr
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2817c549d..fb9116cc2 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -131,12 +131,6 @@ let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
-let constant sl s =
-  constr_of_global
-    (Nametab.locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
-
 let find_reference sl s =
     (Nametab.locate (make_qualid(Names.make_dirpath
 			   (List.map id_of_string (List.rev sl)))
@@ -277,7 +271,6 @@ let cache_Function (_,finfos) =
 
 
 let load_Function _  = cache_Function
-let open_Function _ = cache_Function
 let subst_Function (subst,finfos) =
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
@@ -508,12 +501,6 @@ let jmeq () =
      init_constant ["Logic";"JMeq"] "JMeq")
   with e -> raise (ToShow e)
 
-let jmeq_rec () =
-  try
-    Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
-	  init_constant ["Logic";"JMeq"] "JMeq_rec"
-  with e -> raise (ToShow e)
-
 let jmeq_refl () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 5410e724a..a811b29b8 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -853,17 +853,6 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
   lident , bindlist , Some cstr_expr , lcstor_expr
 
 
-
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
-  match rdecl with
-    | (nme,None,t) ->
-        let traw = Detyping.detype false [] [] t in
-        GProd (Loc.ghost,nme,Explicit,traw,t2)
-    | (_,Some _,_) -> assert false
-
-
-
-
 let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ec1994cd0..a2f16dc6d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -18,7 +18,6 @@ open Globnames
 open Nameops
 open Errors
 open Util
-open Closure
 open Tacticals
 open Tacmach
 open Tactics
@@ -50,10 +49,6 @@ let coq_base_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
     (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
 
-let coq_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition"
-    (Coqlib.init_modules @ Coqlib.arith_modules) s;;
-
 let find_reference sl s =
     (locate (make_qualid(Names.make_dirpath
 			   (List.map id_of_string (List.rev sl)))
@@ -126,7 +121,6 @@ let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
     (pf_type_of gls c)
 let h'_id = id_of_string "h'"
-let heq_id = id_of_string "Heq"
 let teq_id = id_of_string "teq"
 let ano_id = id_of_string "anonymous"
 let x_id = id_of_string "x"
@@ -154,18 +148,12 @@ let le_n = function () -> (coq_base_constant "le_n")
 let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
 let coq_O = function () -> (coq_base_constant "O")
 let coq_S = function () -> (coq_base_constant "S")
-let gt_antirefl = function () -> (coq_constant "gt_irrefl")
 let lt_n_O = function () -> (coq_base_constant "lt_n_O")
-let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn")
-let f_equal = function () -> (coq_constant "f_equal")
-let well_founded_induction = function () -> (coq_constant "well_founded_induction")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
 let max_constr = function () -> (constr_of_global (delayed_force max_ref))
 let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
 
 let f_S t = mkApp(delayed_force coq_S, [|t|]);;
-let make_refl_eq constructor type_of_t t  =
-  mkApp(constructor,[|type_of_t;t|])
 
 let rec n_x_id ids n =
   if n = 0 then []
@@ -960,10 +948,6 @@ let equation_others _ expr_info continuation_tac infos =
       (intros_values_eq expr_info [])
   else continuation_tac infos
 
-let equation_letin (na,b,t,e) expr_info continuation_tac info = 
-  let new_e = subst1 info.info e in 
-  continuation_tac {info with info = new_e;} 
-
 let equation_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
     then intros_values_eq expr_info []
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index e40a8a273..99eadd65d 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -405,9 +405,7 @@ let pplus x y = Mc.PEadd(x,y)
 let pmult x y = Mc.PEmul(x,y)
 let pconst x = Mc.PEc x
 let popp x = Mc.PEopp x
- 
-let debug = false
- 
+
 (* keep track of enumerated vectors *)
 let rec mem p x  l = 
  match l with  [] -> false | e::l -> if p x e then true else mem p x l
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 6722008de..eb713f251 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,9 +16,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Quote
-open Mutils
-open Glob_term
 open Errors
 open Misctypes
 
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 4cac90713..34be7244d 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -8,34 +8,13 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Pp
 open Errors
 open Util
-open Names
 open Term
-open Closure
-open Environ
-open Libnames
 open Tactics
-open Glob_term
-open Tacticals
-open Tacexpr
-open Pcoq
-open Tactic
-open Constr
-open Proof_type
 open Coqlib
-open Tacmach
-open Mod_subst
-open Tacinterp
-open Libobject
-open Printer
-open Declare
-open Decl_kinds
-open Entries
 
 open Num
-open Unix
 open Utile
 
 (***********************************************************************
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 071df5cf7..a610c8461 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -7,9 +7,8 @@
 (************************************************************************)
 
 (* Recursive polynomials: R[x1]...[xn]. *)
-open Utile
-open Errors
 open Util
+open Utile
 
 (* 1. Coefficients: R *)
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ccf397eda..9bfebe348 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -15,21 +15,12 @@
 
 open Errors
 open Util
-open Pp
-open Reduction
-open Proof_type
 open Names
 open Nameops
 open Term
-open Declarations
-open Environ
-open Sign
-open Inductive
 open Tacticals
 open Tacmach
-open Evar_refiner
 open Tactics
-open Clenv
 open Logic
 open Libnames
 open Globnames
@@ -193,8 +184,6 @@ let coq_Zopp = lazy (zbase_constant "Z.opp")
 let coq_Zminus = lazy (zbase_constant "Z.sub")
 let coq_Zsucc = lazy (zbase_constant "Z.succ")
 let coq_Zpred = lazy (zbase_constant "Z.pred")
-let coq_Zgt = lazy (zbase_constant "Z.gt")
-let coq_Zle = lazy (zbase_constant "Z.le")
 let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat")
 let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add")
 let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul")
@@ -326,7 +315,6 @@ let coq_iff = lazy (constant "iff")
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
 (* For unfold *)
-open Closure
 let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
   | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
       EvalConstRef kn
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 6abcc7b6f..800254671 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -17,8 +17,6 @@
 (*   the number of source of numbering.                                   *)
 (**************************************************************************)
 
-open Names
-
 module type INT = sig
   type bigint
   val less_than : bigint -> bigint -> bool
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 42cc6bb1d..abb13efd5 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Pp
 open Tacexpr
 open Quote
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 311ab3081..61a464c1c 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -101,7 +101,6 @@
 
 
 (*i*)
-open Pp
 open Errors
 open Util
 open Names
@@ -110,8 +109,6 @@ open Pattern
 open Patternops
 open Matching
 open Tacmach
-open Tactics
-open Tacexpr
 (*i*)
 
 (*s First, we need to access some Coq constants
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index c1cea8aac..5b57a0d17 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -71,7 +71,6 @@ let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module
 let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module
 
 (* Logic *)
-let coq_eq = lazy(init_constant  "eq")
 let coq_refl_equal = lazy(init_constant  "eq_refl")
 let coq_and = lazy(init_constant "and")
 let coq_not = lazy(init_constant "not")
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index c6256b0c5..e573f2006 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -7,7 +7,6 @@
  *************************************************************************)
 
 open Pp
-open Errors
 open Util
 open Const_omega
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index d1ba173d3..20ec17269 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Errors
 open Util
 open Goptions
@@ -63,15 +62,6 @@ type form=
   | Conjunct of form * form
   | Disjunct of form * form
 
-type tag=int
-
-let decomp_form=function
-    Atom i -> Some (i,[])
-  | Arrow (f1,f2) -> Some (-1,[f1;f2])
-  | Bot -> Some (-2,[])
-  | Conjunct (f1,f2) -> Some (-3,[f1;f2])
-  | Disjunct (f1,f2) -> Some (-4,[f1;f2])
-
 module Fmap=Map.Make(struct type t=form let compare=compare end)
 
 type sequent =
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index c10aece99..ceaf2a79b 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -11,8 +11,6 @@ module Search = Explore.Make(Proof_search)
 open Errors
 open Util
 open Term
-open Names
-open Evd
 open Tacmach
 open Proof_search
 
@@ -29,13 +27,6 @@ let li_False = lazy (destInd (logic_constant "False"))
 let li_and = lazy (destInd (logic_constant "and"))
 let li_or =  lazy (destInd (logic_constant "or"))
 
-let data_constant =
-  Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"]
-
-let l_true_equals_true =
-  lazy (mkApp(logic_constant "eq_refl",
-        [|data_constant "bool";data_constant "true"|]))
-
 let pos_constant =
   Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index abf142e79..f30ab7e8b 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -17,14 +17,9 @@ open Closure
 open Environ
 open Libnames
 open Globnames
-open Tactics
 open Glob_term
 open Tacticals
 open Tacexpr
-open Pcoq
-open Tactic
-open Constr
-open Proof_type
 open Coqlib
 open Tacmach
 open Mod_subst
@@ -75,17 +70,6 @@ and mk_clos_app_but f_map subs f args n =
             (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
       | None -> mk_clos_app_but f_map subs f args (n+1)
 
-
-let interp_map l c =
-  try
-    let (im,am) = List.assoc c l in
-    Some(fun i ->
-      if List.mem i im then Eval
-      else if List.mem i am then Prot
-      else if i = -1 then Eval
-      else Rec)
-  with Not_found -> None
-
 let interp_map l t =
   try Some(List.assoc_f eq_constr t l) with Not_found -> None
 
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 88cc07c0e..03fbc7e98 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -10,13 +10,9 @@ open Pp
 open Errors
 open Util
 open Names
-open Pcoq
 open Glob_term
-open Topconstr
-open Libnames
 open Globnames
 open Coqlib
-open Bigint
 
 exception Non_closed_ascii
 
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5219124cd..8f34ec495 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -9,13 +9,11 @@
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
-open Util
 open Glob_term
 open Bigint
 open Coqlib
 open Pp
 open Errors
-open Util
 (*i*)
 
 (**********************************************************************)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index cdcdc6e62..94d4e0713 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -9,7 +9,6 @@
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
-open Libnames
 open Globnames
 open Glob_term
 
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index d36851ed9..a40c966fe 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -6,13 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Errors
 open Util
 open Names
-open Pcoq
-open Topconstr
-open Libnames
 open Globnames
 
 exception Non_closed_number
@@ -21,7 +16,6 @@ exception Non_closed_number
 (* Parsing R via scopes                                               *)
 (**********************************************************************)
 
-open Libnames
 open Glob_term
 open Bigint
 
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 7474a8b0e..c9767a975 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -6,14 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-open Pp
-open Errors
-open Util
-open Names
-open Pcoq
-open Libnames
 open Globnames
-open Topconstr
 open Ascii_syntax
 open Glob_term
 open Coqlib
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index b1838f4a4..8f1d97d3b 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -15,8 +15,6 @@
 (*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *)
 type types = {synthesized : Term.types ; expected : Term.types option};;
 
-let prerr_endline _ = ();;
-
 let cprop =
  let module N = Names in
   N.make_con
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 4fc1fc2b7..623d7c804 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -13,13 +13,10 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 open Tacexpr;;
-open Decl_mode;;
 open Printer;;
 open Pp;;
 open Environ;;
-open Format;;
 open Proof_type;;
-open Evd;;
 open Termops;;
 open Ppconstr;;
 open Names;;
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index ee9bcb25d..2550e248a 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -35,50 +35,8 @@ let print_proof_tree, set_print_proof_tree =
 
 let print_if_verbose s = if !verbose then print_string s;;
 
-(* Next exception is used only inside print_coq_object and tag_of_string_tag *)
-exception Uninteresting;;
-
-(* NOT USED anymore, we back to the V6 point of view with global parameters
-
-(* Internally, for Coq V7, params of inductive types are associated     *)
-(* not to the whole block of mutual inductive (as it was in V6) but to  *)
-(* each member of the block; but externally, all params are required    *)
-(* to be the same; the following function checks that the parameters    *)
-(* of each inductive of a same block are all the same, then returns     *)
-(* this number; it fails otherwise                                      *)
-let extract_nparams pack =
- let module D = Declarations in
- let module U = Util in
- let module S = Sign in
-
-  let {D.mind_nparams=nparams0} = pack.(0) in
-  let arity0 = pack.(0).D.mind_user_arity in
-  let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in
-  for i = 1 to Array.length pack - 1 do
-    let {D.mind_nparams=nparamsi} = pack.(i) in
-    let arityi = pack.(i).D.mind_user_arity in
-    let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in
-    if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
-  done;
-  nparams0
-
-*)
-
 open Decl_kinds
 
-(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
-(* than that could exists in cooked form with the same name in a super        *)
-(* section of the actual section                                              *)
-let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
-  let tag = Libobject.object_tag o in
-   print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
-   match tag with
-      "CONSTANT"        -> true   (* constants/parameters are non global *)
-    | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
-    | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
-    | _                 -> false  (* uninteresting thing that won't be printed*)
-;;
-
 (* filter_params pvars hyps *)
 (* filters out from pvars (which is a list of lists) all the variables *)
 (* that does not belong to hyps (which is a simple list)               *)
@@ -295,54 +253,6 @@ let mk_variable_obj id body typ =
     (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params)
 ;;
 
-(* Unsharing is not performed on the body, that must be already unshared. *)
-(* The evar map and the type, instead, are unshared by this function.     *)
-let mk_current_proof_obj is_a_variable id bo ty evar_map env =
- let unshared_ty = Unshare.unshare ty in
- let metasenv =
-  List.map
-   (function
-     (n, {Evd.evar_concl = evar_concl ;
-          Evd.evar_hyps = evar_hyps}
-      ) ->
-       (* We map the named context to a rel context and every Var to a Rel *)
-       let final_var_ids,context =
-        let rec aux var_ids =
-         function
-            [] -> var_ids,[]
-          | (n,None,t)::tl ->
-              let final_var_ids,tl' = aux (n::var_ids) tl in
-              let t' = Term.subst_vars var_ids t in
-               final_var_ids,(n, Acic.Decl (Unshare.unshare t'))::tl'
-          | (n,Some b,t)::tl ->
-              let final_var_ids,tl' = aux (n::var_ids) tl in
-              let b' = Term.subst_vars var_ids b in
-               (* t will not be exported to XML. Thus no unsharing performed *)
-               final_var_ids,(n, Acic.Def  (Unshare.unshare b',t))::tl'
-        in
-         aux [] (List.rev (Environ.named_context_of_val evar_hyps))
-       in
-        (* We map the named context to a rel context and every Var to a Rel *)
-        (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))
-   ) (Evarutil.non_instantiated evar_map)
- in
-  let id' = Names.string_of_id id in
-   if metasenv = [] then
-    let ids =
-     Names.Idset.union
-      (Environ.global_vars_set env bo) (Environ.global_vars_set env ty) in
-    let hyps0 = Environ.keep_hyps env ids in
-    let hyps = string_list_of_named_context_list hyps0 in
-    (* Variables are the identifiers of the variables in scope *)
-    let variables = search_variables () in
-    let params = filter_params variables hyps in
-     if is_a_variable then
-      Acic.Variable (id',Some bo,unshared_ty,params)
-     else
-      Acic.Constant (id',Some bo,unshared_ty,params)
-   else
-    Acic.CurrentProof (id',metasenv,bo,unshared_ty)
-;;
 
 let mk_constant_obj id bo ty variables hyps =
  let hyps = string_list_of_named_context_list hyps in
@@ -395,11 +305,6 @@ let theory_output_string ?(do_not_quote = false) s =
    Buffer.add_string theory_buffer s
 ;;
 
-let kind_of_global_goal = function
-  | Global, DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
-  | Global, (Proof k) -> "THEOREM",Kindops.string_of_theorem_kind k
-  | Local, _ -> assert false
-
 let kind_of_inductive isrecord kn =
  "DEFINITION",
  if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite
diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4
index 597190d3e..5ca6e155b 100644
--- a/plugins/xml/xmlentries.ml4
+++ b/plugins/xml/xmlentries.ml4
@@ -14,13 +14,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Util;;
-open Vernacinterp;;
-
-open Extend;;
-open Genarg;;
-open Pp;;
-open Pcoq;;
+open Pp
 
 (* File name *)