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

8 files changed, 12 insertions, 22 deletions

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 9f887fc75..5d2668604 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -151,7 +151,6 @@ END
 (* Guesses the type and calls field_gen with the right theory *)
 let field g =
   Coqlib.check_required_library ["Coq";"field";"Field"];
-  let ist = { lfun=[]; debug=get_debug () } in
   let typ = 
     match Hipattern.match_with_equation (pf_concl g) with
       | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t
diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml
index 876dc6c06..a2a72676c 100644
--- a/contrib/jprover/jall.ml
+++ b/contrib/jprover/jall.ml
@@ -1788,11 +1788,13 @@ struct
       else  if o = ("",Orr,dummyt,dummyt) then  (* Orr is a dummy for no d-gen. rule *)
          ptree
       else
+(*
          let (x1,x2,x3,x4) = r
          and (y1,y2,y3,y4) = o in
-(*   print_endline ("top or_l: "^x1);
+   print_endline ("top or_l: "^x1);
    print_endline ("or_l address: "^addr);
-   print_endline ("top dgen-rule: "^y1); *)
+   print_endline ("top dgen-rule: "^y1);
+*)
          trans_add_branch r o addr "" ptree dglist (subrel,tsubrel)
 
 (* Isolate layer and outer recursion structure *)
@@ -1989,8 +1991,7 @@ struct
                         let (srel,sren) = build_formula_rel dtreelist slist predname in
                         (srel @ rest_rel),(sren @ rest_renlist)
                    | Gamma ->
-                        let n = Array.length suctrees
-                        and succlist = (Array.to_list suctrees) in
+                        let succlist = (Array.to_list suctrees) in
                         let dtreelist = (List.map (fun x -> (1,x)) succlist) in
 (*                if (nonemptys suctrees 0 n) = 1  then
    let (srel,sren) = build_formula_rel dtreelist slist pos.name in
@@ -3039,8 +3040,7 @@ struct
                if (p.pt = Delta) then                 (* keep the tree ordering for the successor position only *)
                   let psucc = List.hd succs in
                   let ppsuccs = tpredsucc psucc ftree in
-                  let pre = List.hd ppsuccs
-                  and sucs = List.tl ppsuccs in
+                  let sucs = List.tl ppsuccs in
                   replace_ordering (psucc.name) sucs redpo (* union the succsets of psucc *)
                else
                   redpo
@@ -4582,7 +4582,6 @@ let gen_prover mult_limit logic calculus hyps concls =
    let (input_map,renamed_termlist) = renam_free_vars (hyps @ concls) in
    let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in
    let sequent_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in
-      let (ptree,count_ax) = bproof sequent_proof in
       let idl = build_formula_id ftree in
 (*      print_ftree ftree;   apple *)
          (* transform types and rename constants *)
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
index 8de7f37d3..58307c334 100644
--- a/contrib/jprover/jprover.ml4
+++ b/contrib/jprover/jprover.ml4
@@ -390,7 +390,7 @@ let dyn_truer =
 (* Do the proof by the guidance of JProver. *)
 
 let do_one_step inf =
-  let (rule, (s1, t1), ((s2, t2) as k)) = inf in
+  let (rule, (s1, t1), (s2, t2)) = inf in
    begin
 (*i   if not (Jterm.is_xnil_term t2) then
    begin
diff --git a/contrib/jprover/jtunify.ml b/contrib/jprover/jtunify.ml
index 2295e62ce..91aa6b4ba 100644
--- a/contrib/jprover/jtunify.ml
+++ b/contrib/jprover/jtunify.ml
@@ -177,7 +177,7 @@ let rec combine subst ((ov,oslist) as one_subst)  =
          else
             (f::rest_combine)
 
-let compose ((n,subst) as sigma) ((ov,oslist) as one_subst) =
+let compose ((n,subst) as _sigma) ((ov,oslist) as one_subst) =
    let com = combine subst one_subst in
 (* begin
    print_endline "!!!!!!!!!test print!!!!!!!!!!";
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index aaabf6533..30562cd44 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -965,7 +965,7 @@ let rec condense p = function
 	let tac',t' = condense (P_APP 2 :: p) t in 
 	(tac @ tac'), Oplus(f,t') 
       end
-  | Oplus(f1,Oz n) as t -> 
+  | Oplus(f1,Oz n) -> 
       let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n)
   | Oplus(f1,f2) -> 
       if weight f1 = weight f2 then begin
@@ -1035,7 +1035,6 @@ let replay_history tactic_normalisation =
 	  let p_initial = [P_APP 2;P_TYPE] in
 	  let tac = shuffle_cancel p_initial e1.body in
 	  let solve_le =
-            let superieur = Lazy.force coq_SUPERIEUR in
             let not_sup_sup = mkApp (build_coq_eq (), [| 
 					Lazy.force coq_relation; 
 					Lazy.force coq_SUPERIEUR;
@@ -1095,17 +1094,13 @@ let replay_history tactic_normalisation =
 	      tclTHEN (mk_then tac) reflexivity ]
 	    
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
-	  let id = hyp_of_tag e1.id in
 	  let c = floor_div e1.constant k in
 	  let d = Bigint.sub e1.constant (Bigint.mult c k) in
 	  let e2 =  {id=e1.id; kind=EQUA;constant = c; 
                      body = map_eq_linear (fun c -> c / k) e1.body } in
-	  let eq1 = val_of(decompile e1) 
-	  and eq2 = val_of(decompile e2) in
+	  let eq2 = val_of(decompile e2) in
 	  let kk = mk_integer k 
 	  and dd = mk_integer d in
-	  let rhs = mk_plus (mk_times eq2 kk) dd in
-	  let state_eq = mk_eq eq1 rhs in
 	  let tac = scalar_norm_add [P_APP 2] e2.body in
 	  tclTHENS 
 	    (cut (mk_gt dd izero)) 
@@ -1419,8 +1414,6 @@ let coq_omega gl =
 let coq_omega = solver_time coq_omega
 
 let nat_inject gl =
-  let aux = id_of_string "auxiliary" in
-  let table = Hashtbl.create 7 in
   let rec explore p t = 
     try match destructurate_term t with
       | Kapp(Plus,[t1;t2]) ->
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index 7b6361afe..69e57ca42 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -425,7 +425,7 @@ let redundancy_elimination new_eq_id system =
            end else begin
              match optinvert with 
                 Some v ->
-                  let kept =
+                  let _kept =
                     if v.constant >? nx.constant 
                     then begin add_event (FORGET_I (v.id,nx.id));v end
                     else begin add_event (FORGET_I (nx.id,v.id));nx end in
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index c22c1dfb5..f554b85f5 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -17,7 +17,6 @@ type result =
 
 let destructurate t =
   let c, args = Term.decompose_app t in
-  let env = Global.env() in
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 6bc693a13..f1aff8d08 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -604,7 +604,7 @@ let rec condense env = function
 	let tac',t' = condense env t in 
 	[do_both (do_list tac) (do_list tac')], Oplus(f,t') 
       end
-  | (Oplus(f1,Oint n) as t) -> 
+  | Oplus(f1,Oint n) -> 
       let tac,f1' = reduce_factor f1 in 
       [do_left (do_list tac)],Oplus(f1',Oint n)
   | Oplus(f1,f2) ->