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, 19 insertions, 31 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 79b048979..28e8c4139 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -427,7 +427,7 @@ let unify_tomatch_with_patterns isevars env tmloc typ = function
   | Some (cloc,(cstr,_ as c)) ->
       (let tyi = inductive_of_constructor c in
        try 
-	 let indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in
+	 let _indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in
 	 IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
        with NotCoercible ->
 	 (* 2 cases : Not the right inductive or not an inductive at all *)
@@ -782,7 +782,6 @@ let build_aliases_context env sigma names allpats pats =
 	let newallpats =
 	  List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in
 	let oldallpats = List.map List.tl oldallpats in
-	let u = Retyping.get_type_of env sigma deppat in
 	let decl = (na,Some deppat,t) in
 	let a = (deppat,nondeppat,d,t) in
 	insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1) 
@@ -918,7 +917,6 @@ let abstract_conclusion typ cs =
   lam_it p sign
 
 let infer_predicate loc env isevars typs cstrs indf =
-  let (mis,_) = dest_ind_family indf in
   (* Il faudra substituer les isevars a un certain moment *)
   if Array.length cstrs = 0 then (* "TODO4-3" *)
     error "Inference of annotation for empty inductive types not implemented"
@@ -930,7 +928,10 @@ let infer_predicate loc env isevars typs cstrs indf =
     in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
-(*    let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in*)
+(*
+    let (mis,_) = dest_ind_family indf in
+    let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
+*)
     let (sign,_) = get_arity env indf in
     let mtyp =
       if array_exists is_Type typs then
@@ -980,7 +981,7 @@ let rec map_predicate f k = function
 let rec noccurn_predicate k = function
   | PrCcl ccl -> noccurn k ccl
   | PrProd pred -> noccurn_predicate (k+1) pred
-  | PrLetIn ((names,dep as tm),pred) ->
+  | PrLetIn ((names,dep),pred) ->
       let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
       noccurn_predicate (k+k') pred
 
@@ -1191,7 +1192,7 @@ let group_equations pb mind current cstrs mat =
 		 let rest = {rest with tag = lower_pattern_status rest.tag} in
 		 brs.(i-1) <- (args, rest) :: brs.(i-1)
 	       done
-	   | PatCstr (loc,((_,i) as cstr),args,_) as pat ->
+	   | PatCstr (loc,((_,i)),args,_) ->
 	       (* This is a regular clause *)
 	       only_default := false;
 	       brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in
@@ -1240,8 +1241,6 @@ let build_branch current deps pb eqns const_info =
     else 
       DepAlias
   in
-  let partialci =
-    applist (mkConstruct const_info.cs_cstr, const_info.cs_params) in
   let history = 
     push_history_pattern const_info.cs_nargs
       (AliasConstructor const_info.cs_cstr)
@@ -1339,7 +1338,7 @@ and match_current pb ((current,typ as ct),deps) =
 	if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt  then
 	  compile (shift_problem ct pb)
 	else
-          let constraints = Array.map (solve_constraints indt) cstrs in
+          let _constraints = Array.map (solve_constraints indt) cstrs in
 
 	  (* We generalize over terms depending on current term to match *)
 	  let pb = generalize_problem pb current deps in
@@ -1444,7 +1443,7 @@ let prepare_initial_alias_eqn isdep tomatchl eqn =
     (fun pat (tm,tmtyp) (subst, stripped_pats) ->
        match alias_of_pat pat with
 	 | Anonymous -> (subst, pat::stripped_pats)
-	 | Name idpat as na ->
+	 | Name idpat ->
 	     match kind_of_term tm with
 	       | Rel n when not (is_dependent_indtype tmtyp) & not isdep
 		   -> (n, idpat)::subst, (unalias_pat pat::stripped_pats)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 1eccc645d..cc3725210 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -100,7 +100,6 @@ let clenv_environments_evars env evd bound c =
       | (n, Prod (na,c1,c2)) ->
           let e',constr = Evarutil.new_evar e env c1 in
 	  let dep = dependent (mkRel 1) c2 in
-	  let na' = if dep then na else Anonymous in
 	  clrec (e', constr::ts) (option_app ((+) (-1)) n)
 	    (if dep then (subst1 constr c2) else c2)
       | (n, LetIn (na,b,_,c)) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 835f1e00d..a0c605857 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -78,7 +78,7 @@ let evar_apprec_nobeta env isevars stack c =
 let evar_apprec env isevars stack c =
   let sigma = evars_of isevars in
   let rec aux s =
-    let (t,stack as s') = Reductionops.apprec env sigma s in
+    let (t,stack) = Reductionops.apprec env sigma s in
     match kind_of_term t with
       | Evar (n,_ as ev) when Evd.is_defined sigma n ->
 	  aux (Evd.existential_value sigma ev, stack)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ce8aa4844..12559d1da 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -183,7 +183,7 @@ let make_evar_instance_with_rel env =
 
 let make_subst env args =
   snd (fold_named_context
-    (fun env (id,b,c) (args,l as g) ->
+    (fun env (id,b,c) (args,l) ->
        match b, args with
 	 | (* None *) _ , a::rest -> (rest, (id,a)::l)
 (*	 | Some _, _ -> g*)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e58609195..ea21efcc4 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -248,7 +248,6 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 let mis_make_indrec env sigma listdepkind mib =
   let nparams = mib.mind_nparams in
   let nparrec = mib. mind_nparams_rec in
-  let lnamespar = mib.mind_params_ctxt in
   let lnonparrec,lnamesparrec = 
     list_chop (nparams-nparrec) mib.mind_params_ctxt in
   let nrec = List.length listdepkind in
@@ -380,7 +379,6 @@ let mis_make_indrec env sigma listdepkind mib =
 	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
 	      let recarg = recargpar@recarg in
 	      let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
-	      let indf = (indi, vargs) in
 	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
 	      let p_0 =
 		type_rec_branch
@@ -532,7 +530,6 @@ let type_rec_branches recursive env sigma indt p c =
   let tyi = snd ind in
   let init_depPvec i = if i = tyi then Some(true,p) else None in
   let depPvec = Array.init mib.mind_ntypes init_depPvec in
-  let vargs = Array.of_list params in
   let constructors = get_constructors env indf in
   let lft =
     array_map2
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c540a4a1f..d0dca036e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -194,7 +194,6 @@ let build_dependent_constructor cs =
 
 let build_dependent_inductive env ((ind, params) as indf) =
   let arsign,_ = get_arity env indf in
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let nrealargs = List.length arsign in
   applist 
     (mkInd ind,
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 6e06f978f..c67917477 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -129,7 +129,7 @@ let rec inst lvar = function
   (* Non recursive *)
   | (PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x 
   (* Bound to terms *)
-  | (PFix _ | PCoFix _ as r) ->
+  | (PFix _ | PCoFix _) ->
       error ("Not instantiable pattern")
 
 let rec subst_pattern subst pat = match pat with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 497739692..148be3991 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -403,7 +403,7 @@ let rec pretype tycon env isevars lvar = function
 
   | RLetTuple (loc,nal,(na,po),c,d) ->
       let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs) as indt) = 
+      let (IndType (indf,realargs)) = 
 	try find_rectype env (evars_of !isevars) cj.uj_type
 	with Not_found ->
 	  let cloc = loc_of_rawconstr c in
@@ -441,7 +441,6 @@ let rec pretype tycon env isevars lvar = function
 	       let mis,_ = dest_ind_family indf in
 	       let ci = make_default_case_info env LetStyle mis in
 	       mkCase (ci, p, cj.uj_val,[|f|]) in 
-             let cs = build_dependent_constructor cs in
 	     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
 	 | None -> 
@@ -550,7 +549,6 @@ let rec pretype tycon env isevars lvar = function
 	       else pretype (mk_tycon bty.(0)) env isevars lvar f 
 	     in
 	     let fv = fj.uj_val in
-	     let ft = fj.uj_type in
 	     let v =
 	       let mis,_ = dest_ind_family indf in
 	       let ci = make_default_case_info env st mis in
@@ -661,7 +659,7 @@ let rec pretype tycon env isevars lvar = function
 
   | RIf (loc,c,(na,po),b1,b2) ->
       let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs) as indt) = 
+      let (IndType (indf,realargs)) = 
 	try find_rectype env (evars_of !isevars) cj.uj_type
 	with Not_found ->
 	  let cloc = loc_of_rawconstr c in
@@ -799,8 +797,6 @@ let rec pretype tycon env isevars lvar = function
           let (ind,params) = dest_ind_family indf in
           let (mib,mip) = lookup_mind_specif env ind in
           let recargs = mip.mind_recargs in
-          let mI = mkInd ind in
-          let nconstr = Array.length mip.mind_consnames in
           let tyi = snd ind in
           if isrec && mis_is_recursive_subset [tyi] recargs then
             Some (Detyping.detype (false,env)
@@ -976,7 +972,7 @@ let check_evars env initial_sigma isevars c =
   let sigma = evars_of !isevars in
   let rec proc_rec c =
     match kind_of_term c with
-      | Evar (ev,args as k) ->
+      | Evar (ev,args) ->
           assert (Evd.in_dom sigma ev);
 	  if not (Evd.in_dom initial_sigma ev) then
             let (loc,k) = evar_source ev !isevars in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7476dc0a7..67c0fc856 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -188,7 +188,7 @@ let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
 
 let reduce_mind_case mia =
   match kind_of_term mia.mconstr with
-    | Construct (ind_sp,i as cstr_sp) ->
+    | Construct (ind_sp,i) ->
 (*	let ncargs = (fst mia.mci).(i-1) in*)
 	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
         applist (mia.mlf.(i-1),real_cargs)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 117b626ea..c9189ad2f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -224,7 +224,7 @@ let compute_consteval_mutual_fix sigma env ref =
     match kind_of_term c' with
       | Lambda (na,t,g) when l=[] ->
 	  srec (push_rel (na,None,t) env) (minarg+1) (t::labs) ref g
-      | Fix ((lv,i),(names,_,_) as fix) ->
+      | Fix ((lv,i),(names,_,_)) ->
 	  (* Last known constant wrapping Fix is ref = [labs](Fix l) *)
 	  (match compute_consteval_direct sigma env ref with
 	     | NotAnElimination -> (*Above const was eliminable but this not!*)
@@ -360,7 +360,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
 
 let reduce_mind_case_use_function func env mia =
   match kind_of_term mia.mconstr with 
-    | Construct(ind_sp,i as cstr_sp) ->
+    | Construct(ind_sp,i) ->
 	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
 	applist (mia.mlf.(i-1), real_cargs)
     | CoFix (_,(names,_,_) as cofix) ->
@@ -592,7 +592,6 @@ let is_head c t =
 let contextually byhead (locs,c) f env sigma t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref 1 in
-  let check = ref true in
   let except = List.exists (fun n -> n<0) locs in
   if except & (List.exists (fun n -> n>=0) locs) 
   then error "mixing of positive and negative occurences"
@@ -799,7 +798,7 @@ let pattern_occs loccs_trm env sigma c =
 exception NotStepReducible
 
 let one_step_reduce env sigma c = 
-  let rec redrec (x, largs as s) =
+  let rec redrec (x, largs) =
     match kind_of_term x with
       | Lambda (n,t,c)  ->
           (match decomp_stack largs with
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index ee1bfe4d6..1a6521d98 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -614,7 +614,6 @@ let replace_term = replace_term_gen eq_constr
 let subst_term_occ_gen locs occ c t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
-  let check = ref true in
   let except = List.exists (fun n -> n<0) locs in
   if except & (List.exists (fun n -> n>=0) locs) 
   then error "mixing of positive and negative occurences"