Removing dead code and unused opens.

21 files changed, 1 insertions, 79 deletions

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