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

9 files changed, 9 insertions, 15 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index af00edd65..577ea5cb2 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -842,7 +842,7 @@ let strip_update_shift_app head stk =
   let rec strip_rec rstk h depth = function
     | Zshift(k) as e :: s ->
         strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
-    | (Zapp args :: s) as stk ->
+    | (Zapp args :: s) ->
         strip_rec (Zapp args :: rstk)
           {norm=h.norm;term=FApp(h,Array.of_list args)} depth s
     | Zupdate(m)::s ->
@@ -885,7 +885,7 @@ let get_arg h stk =
 let rec get_args n tys f e stk =
   match stk with
       Zupdate r :: s ->
-        let hd = update r (Cstr,FLambda(n,tys,f,e)) in
+        let _hd = update r (Cstr,FLambda(n,tys,f,e)) in
         get_args n tys f e s
     | Zshift k :: s ->
         get_args n tys f (subs_shft (k,e)) s
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 73e10df65..f743970c6 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -146,7 +146,6 @@ and slot_for_fv env fv=
 	    set_relval rv v; v
 	| VKdef(c,e) ->
 	    let v = val_of_constr e c in
-	    let k = nb_rel e in
 	    set_relval rv v; v
       end
  
@@ -158,7 +157,6 @@ and eval_to_patch env (buff,pl,fv) =
 	patch_int buff pos (slot_for_getglobal env kn)
   in 
   List.iter patch pl;
-  let nfv = Array.length fv in
   let vm_env = Array.map (slot_for_fv env) fv in 
   let tc = tcode_of_code buff (length buff) in
   eval_tcode tc vm_env
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 25464a3ce..67a0f850c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -454,7 +454,6 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
       (fun c ->
         let c = body_of_type c in
         let sign, rawc = mind_extract_params nparams c in
-        let env' = push_rel_context sign env in
         try
 	  check_constructors ienv true nparams rawc
         with IllFormedInd err -> 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bf64dfda0..235c82b1a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -593,7 +593,6 @@ let check_one_fix renv recpos def =
       | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
           List.for_all (check_rec_call renv) l &&
           array_for_all (check_rec_call renv) typarray && 
-	  let nbfix = Array.length typarray in
           let decrArg = recindxs.(i) in
           let renv' = push_fix_renv renv recdef in 
           if (List.length l < (decrArg+1)) then
@@ -613,7 +612,7 @@ let check_one_fix renv recpos def =
                 bodies in
             array_for_all (fun b -> b) ok_vect
 
-      | Const kn as c -> 
+      | Const kn -> 
           (try List.for_all (check_rec_call renv) l
            with (FixGuardError _ ) as e ->
              if evaluable_constant kn renv.env then 
@@ -705,7 +704,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   (Array.map fst rv, Array.map snd rv)
 
 
-let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
+let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) =
   let (minds, rdef) = inductive_of_mutfix env fix in
   for i = 0 to Array.length bodies - 1 do
     let (fenv,body) = rdef.(i) in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index e0d16d499..c6afb1da0 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -45,7 +45,6 @@ let empty_subst = Umap.empty
 let add_msid msid mp =
   Umap.add (MSI msid) (mp,None)
 let add_mbid mbid mp resolve =
- let mp' = MBI mbid in
   Umap.add (MBI mbid) (mp,resolve)
 
 let map_msid msid mp = add_msid msid mp empty_subst
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f87dc90e4..5ab9f9a02 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -174,7 +174,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
 	       check_conv cst conv env c1 c2
       in
        cst
-   | IndType ((kn,i) as ind,mind1) ->
+   | IndType ((kn,i),mind1) ->
       Util.error ("The kernel does not recognize yet that a parameter can be " ^
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
diff --git a/kernel/term.ml b/kernel/term.ml
index b86ac850c..8bd079ce5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -748,7 +748,7 @@ let substl laml =
   substn_many (Array.map make_substituend (Array.of_list laml)) 0
 let subst1 lam = substl [lam]
 
-let substl_decl laml (id,bodyopt,typ as d) =
+let substl_decl laml (id,bodyopt,typ) =
   match bodyopt with
     | None -> (id,None,substl laml typ)
     | Some body -> (id, Some (substl laml body), type_app (substl laml) typ)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index cdc9fa0f7..8a2ced1d2 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -80,9 +80,9 @@ and conv_whd pb k whd1 whd2 cu =
       else raise NotConvertible
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> 
       conv_atom pb k a1 stk1 a2 stk2 cu
-  | _, Vatom_stk(Aiddef(_,v) as a2,stk) -> 
+  | _, Vatom_stk(Aiddef(_,v),stk) -> 
       conv_whd pb k whd1 (force_whd v stk) cu
-  | Vatom_stk(Aiddef(_,v) as a1,stk), _ -> 
+  | Vatom_stk(Aiddef(_,v),stk), _ -> 
       conv_whd pb k (force_whd v stk) whd2 cu
   | _, _ -> raise NotConvertible
 
@@ -343,7 +343,7 @@ let type_of_ind env ind =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_nf_arity
 
-let build_branches_type (mind,_ as ind) mib mip params dep p rtbl =
+let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl =
   (* [build_one_branch i cty] construit le type de la ieme branche (commence
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 0aa4f1ff4..8f0d2ebdd 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -318,7 +318,6 @@ let val_of_constant_def n c v =
 
 
 let rec whd_accu a stk =
-  let n = nargs_of_accu a in
   let stk = 
     if nargs_of_accu a = 0 then stk
     else Zapp (args_of_accu a) :: stk in