From f461e7657cab9917c5b405427ddba3d56f197efb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 8 May 2016 18:59:55 +0200 Subject: Removing dead code and unused opens. --- plugins/cc/ccalgo.ml | 5 ----- plugins/cc/g_congruence.ml4 | 2 -- plugins/decl_mode/g_decl_mode.ml4 | 1 - plugins/derive/g_derive.ml4 | 2 -- plugins/extraction/extract_env.ml | 1 - plugins/extraction/g_extraction.ml4 | 1 - plugins/extraction/json.ml | 5 ----- plugins/extraction/modutil.ml | 8 ------- plugins/firstorder/g_ground.ml4 | 1 - plugins/firstorder/instances.ml | 3 --- plugins/fourier/fourierR.ml | 1 - plugins/funind/functional_principles_proofs.ml | 1 - plugins/funind/g_indfun.ml4 | 3 --- plugins/funind/recdef.ml | 2 +- plugins/micromega/coq_micromega.ml | 2 -- plugins/micromega/g_micromega.ml4 | 5 ----- plugins/omega/g_omega.ml4 | 1 - plugins/quote/g_quote.ml4 | 3 --- plugins/romega/g_romega.ml4 | 1 - plugins/setoid_ring/g_newring.ml4 | 1 - plugins/setoid_ring/newring.ml | 31 -------------------------- 21 files changed, 1 insertion(+), 79 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3