From 4a7555cd875b0921368737deed4a271450277a04 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 8 Nov 2005 17:14:52 +0000 Subject: Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/auto.ml | 2 +- tactics/eauto.ml4 | 5 ++--- tactics/elim.ml | 1 - tactics/equality.ml | 6 ++---- tactics/hipattern.ml | 2 +- tactics/inv.ml | 3 --- tactics/leminv.ml | 2 +- tactics/refine.ml | 2 +- tactics/setoid_replace.ml | 2 -- tactics/tacinterp.ml | 17 +++++++---------- tactics/tactics.ml | 9 ++------- 11 files changed, 17 insertions(+), 34 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 0fda09a9a..dd07c2b90 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -670,7 +670,7 @@ and my_find_search db_list local_db hdc concl = (local_db::db_list) in List.map - (fun ({pri=b; pat=p; code=t} as patac) -> + (fun {pri=b; pat=p; code=t} -> (b, match t with | Res_pf (term,cl) -> unify_resolve (term,cl) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 79753ac73..52f5f011a 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -74,8 +74,7 @@ let e_constructor_tac boundopt i lbind gl = let cl = pf_concl gl in let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in let nconstr = - Array.length (snd (Global.lookup_inductive mind)).mind_consnames - and sigma = project gl in + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in if i=0 then error "The constructors are numbered starting from 1"; if i > nconstr then error "Not enough constructors"; begin match boundopt with @@ -217,7 +216,7 @@ and e_my_find_search db_list local_db hdc concl = list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) in let tac_of_hint = - fun ({pri=b; pat = p; code=t} as patac) -> + fun {pri=b; pat = p; code=t} -> (b, let tac = match t with diff --git a/tactics/elim.ml b/tactics/elim.ml index 6a91cbc94..90b3c66b2 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -181,7 +181,6 @@ let double_ind h1 h2 gls = if abs_i < abs_j then (abs_i,abs_j) else if abs_i > abs_j then (abs_j,abs_i) else error "Both hypotheses are the same" in - let cl = pf_concl gls in (tclTHEN (tclDO abs_i intro) (onLastHyp (fun id -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 4797146a3..57d9ab58a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -314,7 +314,7 @@ let discriminable env sigma t1 t2 = the continuation then constructs the case-split. *) let descend_then sigma env head dirn = - let IndType (indf,_) as indt = + let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> assert false in let ind,_ = dest_ind_family indf in @@ -357,7 +357,7 @@ let descend_then sigma env head dirn = giving [True], and all the rest giving False. *) let construct_discriminator sigma env dirn c sort = - let (IndType(indf,_) as indt) = + let IndType(indf,_) = try find_rectype env sigma (type_of env sigma c) with Not_found -> (* one can find Rel(k) in case of dependent constructors @@ -392,7 +392,6 @@ let rec build_discriminator sigma env dirn c sort = function try find_rectype env sigma cty with Not_found -> assert false in let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in - let _,arsort = get_arity env indf in let nparams = mib.mind_nparams in let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in let newc = mkRel(cnum_nlams-(argnum-nparams)) in @@ -434,7 +433,6 @@ let discrEq (lbeq,(t,t1,t2)) id gls = let e_env = push_named (e,None,t) env in let discriminator = build_discriminator sigma e_env dirn (mkVar e) sort cpath in - let (indt,_) = find_mrectype env sigma t in let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq gls in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index c3735b2c8..b91222ae9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -300,7 +300,7 @@ let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref let match_sigma ex ex_pat = match matches (Lazy.force ex_pat) ex with - | [(m1,a);(m2,p);(m3,car);(m4,cdr)] as l -> + | [(m1,a);(m2,p);(m3,car);(m4,cdr)] -> assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4); (a,p,car,cdr) | _ -> diff --git a/tactics/inv.ml b/tactics/inv.ml index 75cb66778..57630c964 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -134,7 +134,6 @@ let make_inv_predicate env sigma indf realargs id status concl = else make_iterated_tuple env' sigma ai (xi,ti) in - let sort = get_sort_of env sigma concl in let eq_term = Coqlib.build_coq_eq () in let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist @@ -305,7 +304,6 @@ let remember_first_eq id x = if !x = None then x := Some id a rewrite rule. It erases the clause which is given as input *) let projectAndApply thin id eqname names depids gls = - let env = pf_env gls in let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id))) (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) @@ -400,7 +398,6 @@ let rewrite_equations othin neqns names ba gl = let (depids,nodepids) = split_dep_and_nodep ba.assums gl in let rewrite_eqns = let first_eq = ref None in - let update id = if !first_eq = None then first_eq := Some id in match othin with | Some thin -> tclTHENSEQ diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 1a221dd16..60d05ec70 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -263,8 +263,8 @@ let inversion_lemma_from_goal n na id sort dep_option inv_op = let gl = nth_goal_of_pftreestate n pts in let t = pf_get_hyp_typ gl id in let env = pf_env gl and sigma = project gl in - let fv = global_vars env t in (* Pourquoi ??? + let fv = global_vars env t in let thin_ids = thin_ids (hyps,fv) in if not(list_subset thin_ids fv) then errorlabstrm "lemma_inversion" diff --git a/tactics/refine.ml b/tactics/refine.ml index d53310c66..493232d3c 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -251,7 +251,7 @@ let rec compute_metamap env c = match kind_of_term c with * Réalise le 3. ci-dessus *) -let rec tcc_aux subst (TH (c,mm,sgp) as th) gl = +let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = let c = substl subst c in match (kind_of_term c,sgp) with (* mv => sous-but : on ne fait rien *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 3db8be9dc..5cd163364 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -527,7 +527,6 @@ let what_edited id = let check_is_dependent n args_ty output = let m = List.length args_ty - n in let args_ty_quantifiers, args_ty = Util.list_chop n args_ty in - let delift n = substl (Array.to_list (Array.make n (mkRel 1) (* dummy *))) in let rec aux m t = match kind_of_term t with Prod (n,s,t) when m > 0 -> @@ -648,7 +647,6 @@ let apply_to_relation subst rel = mkApp (rel.rel_Xreflexive_relation_class, subst) } let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = - let env = Global.env() in let lem = match lemma_infos with None -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 79b3b330d..5948da2b8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -385,7 +385,6 @@ let adjust_loc loc = if !strict_check then dummy_loc else loc (* Globalize a name which must be bound -- actually just check it is bound *) let intern_hyp ist (loc,id as locid) = - let (_,env) = get_current_context () in if not !strict_check then locid else if find_ident id ist then @@ -396,7 +395,7 @@ let intern_hyp ist (loc,id as locid) = let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id) let intern_int_or_var ist = function - | ArgVar locid as x -> ArgVar (intern_hyp ist locid) + | ArgVar locid -> ArgVar (intern_hyp ist locid) | ArgArg n as x -> x let intern_inductive ist = function @@ -404,7 +403,7 @@ let intern_inductive ist = function | r -> ArgArg (Nametab.global_inductive r) let intern_global_reference ist = function - | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id) + | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) | r -> let loc,qid = qualid_of_reference r in try ArgArg (loc,locate_global qid) @@ -497,7 +496,7 @@ let intern_clause_pattern ist (l,occl) = let intern_induction_arg ist = function | ElimOnConstr c -> ElimOnConstr (intern_constr ist c) | ElimOnAnonHyp n as x -> x - | ElimOnIdent (loc,id) as x -> + | ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) ElimOnConstr (intern_constr ist (CRef (Ident (dummy_loc,id)))) @@ -506,7 +505,7 @@ let intern_induction_arg ist = function (* Globalizes a reduction expression *) let intern_evaluable ist = function - | Ident (loc,id) as r when find_ltacvar id ist -> ArgVar (loc,id) + | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id) | Ident (_,id) when (not !strict_check & find_hyp id ist) or find_ctxvar id ist -> ArgArg (EvalVarRef id, None) @@ -749,8 +748,6 @@ let rec intern_atomic lf ist x = let _ = lookup_tactic opn in TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l) | TacAlias (loc,s,l,(dir,body)) -> - let (l1,l2) = ist.ltacvars in - let ist' = { ist with ltacvars = ((List.map fst l)@l1,l2) } in let l = List.map (fun (id,a) -> (strip_meta id,intern_genarg ist a)) l in try TacAlias (loc,s,l,(dir,body)) with e -> raise (locate_error_in_file (string_of_dirpath dir) e) @@ -1036,7 +1033,7 @@ let get_debug () = !debug let interp_ident ist id = try match List.assoc id ist.lfun with | VIntroPattern (IntroIdentifier id) -> id - | VConstr c as v when isVar c -> + | VConstr c when isVar c -> (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *) (* c is then expected not to belong to the proof context *) (* would be checkable if env were known from interp_ident *) @@ -1048,7 +1045,7 @@ let interp_ident ist id = let interp_intro_pattern_var ist id = try match List.assoc id ist.lfun with | VIntroPattern ipat -> ipat - | VConstr c as v when isVar c -> + | VConstr c when isVar c -> (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *) (* c is then expected not to belong to the proof context *) (* would be checkable if env were known from interp_ident *) @@ -1076,7 +1073,7 @@ let is_variable env id = List.mem id (ids_of_named_context (Environ.named_context env)) let variable_of_value env = function - | VConstr c as v when isVar c -> destVar c + | VConstr c when isVar c -> destVar c | VIntroPattern (IntroIdentifier id) when is_variable env id -> id | _ -> raise Not_found diff --git a/tactics/tactics.ml b/tactics/tactics.ml index abb86ffde..5079a1010 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -871,8 +871,7 @@ let constructor_tac boundopt i lbind gl = let cl = pf_concl gl in let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in let nconstr = - Array.length (snd (Global.lookup_inductive mind)).mind_consnames - and sigma = project gl in + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in if i=0 then error "The constructors are numbered starting from 1"; if i > nconstr then error "Not enough constructors"; begin match boundopt with @@ -1373,7 +1372,7 @@ let cook_sign hyp0 indvars env = in let _ = fold_named_context seek_deps env ~init:None in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) - let compute_lstatus lhyp (hyp,_,_ as d) = + let compute_lstatus lhyp (hyp,_,_) = if hyp = hyp0 then raise (Shunt lhyp); if List.mem hyp !ldeps then begin lstatus := (hyp,lhyp)::!lstatus; @@ -1476,7 +1475,6 @@ let error_ind_scheme s = (* Check that the elimination scheme has a form similar to the elimination schemes built by Coq *) let compute_elim_signature elimt names_info = - let nparams = ref 0 in let hyps,ccl = decompose_prod_assum elimt in let n = List.length hyps in if n = 0 then error_ind_scheme ""; @@ -1895,7 +1893,6 @@ let interpretable_as_section_decl d1 d2 = match d1,d2 with | (_,None,t1), (_,_,t2) -> eq_constr t1 t2 let abstract_subproof name tac gls = - let env = Global.env() in let current_sign = Global.named_context() and global_sign = pf_hyps gls in let sign,secsign = @@ -1923,7 +1920,6 @@ let abstract_subproof name tac gls = in (* Faudrait un peu fonctionnaliser cela *) let cd = Entries.DefinitionEntry const in let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in - let newenv = Global.env() in constr_of_global (ConstRef con) in exact_no_check @@ -1940,7 +1936,6 @@ let tclABSTRACT name_op tac gls = let admit_as_an_axiom gls = - let env = Global.env() in let current_sign = Global.named_context() and global_sign = pf_hyps gls in let sign,secsign = -- cgit v1.2.3