Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09

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

11 files changed, 17 insertions, 34 deletions

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 =