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

75 files changed, 132 insertions, 231 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) -> 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 956a275a9..48bb19cb6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -807,7 +807,7 @@ object(self)
 				 goal_nb
 				 (if goal_nb<=1 then "" else "s"));
 	  List.iter
-	    (fun ((_,_,_,(s,_)) as hyp) -> 
+	    (fun ((_,_,_,(s,_)) as _hyp) -> 
 	       proof_buffer#insert (s^"\n"))
 	    hyps;
 	  proof_buffer#insert (String.make 38 '_' ^ "(1/"^
@@ -1364,7 +1364,6 @@ Please restart and report NOW.";
 		 if Mutex.try_lock c#lock then begin
 		   c#clear ();
 		   let current_gls = try get_current_goals () with _ -> [] in
-		   let gls_nb = List.length current_gls in
 		   
 		   let set_goal i (s,t) = 
 		     let gnb = string_of_int i in
@@ -1481,19 +1480,17 @@ Please restart and report NOW.";
       (input_view#event#connect#key_press self#active_keypress_handler);
     prerr_endline "CONNECTED active : ";
     print_id (out_some act_id);
-    let dir = (match 
-		 (out_some ((Vector.get input_views index).analyzed_view))
-		 #filename 
-	       with
-	       | None -> ()
-	       | Some f ->     
-		   if not (is_in_coq_path f) then 
-		     begin
-		       let dir = Filename.dirname f in
-		       ignore (Coq.interp false
-				 (Printf.sprintf "Add LoadPath \"%s\". "  dir))
-		     end)
-    in ()
+    match 
+      (out_some ((Vector.get input_views index).analyzed_view)) #filename 
+    with
+      | None -> ()
+      | Some f ->     
+	  if not (is_in_coq_path f) then 
+	    begin
+	      let dir = Filename.dirname f in
+	      ignore (Coq.interp false
+		(Printf.sprintf "Add LoadPath \"%s\". "  dir))
+	    end
 
       
       
@@ -1832,7 +1829,7 @@ let main files =
   let load_f () = 	  
     match select_file ~title:"Load file" () with 
     | None -> ()
-    | (Some f) as fn -> load f
+    | Some f -> load f
   in
   ignore (load_m#connect#activate (load_f));
 
@@ -1906,7 +1903,7 @@ let main files =
   let saveall_f () = 
     Vector.iter
       (function 
-	 | {view = view ; analyzed_view = Some av} as full -> 
+	 | {view = view ; analyzed_view = Some av} -> 
 	     begin match av#filename with 
 	     | None -> ()
 	     | Some f ->
@@ -1929,7 +1926,7 @@ let main files =
   let revert_f () = 
     Vector.iter 
       (function 
-	   {view = view ; analyzed_view = Some av} as full -> 
+	   {view = view ; analyzed_view = Some av} -> 
 	     (try 
 		match av#filename,av#stats with 
 		| Some f,Some stats -> 
@@ -2359,7 +2356,7 @@ let main files =
   let auto_save_f () = 
     Vector.iter 
       (function 
-	   {view = view ; analyzed_view = Some av} as full -> 
+	   {view = view ; analyzed_view = Some av} -> 
 	     (try 
 		av#auto_save
 	      with _ -> ())
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e8cccf9cc..a71d14c82 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -228,7 +228,7 @@ let rec print_list print fmt = function
 
 let browse f url =
   let l,r = !current.cmd_browse in
-  let (s,res) = System.run_command try_convert f (l ^ url ^ r) in
+  let _ = System.run_command try_convert f (l ^ url ^ r) in
   ()
 
 let url_for_keyword =
diff --git a/ide/undo.ml b/ide/undo.ml
index dc723db9d..0b4ea1726 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -107,8 +107,8 @@ object(self)
 		   Queue.iter (fun e -> Stack.push e history) redo;
 		   Queue.clear redo;
 		 end;
-		 let pos = it#offset in
-(*		 if Stack.is_empty history or 
+(*		 let pos = it#offset in
+		 if Stack.is_empty history or 
 		   s=" " or s="\t" or s="\n" or
 					(match Stack.top history with 
 					   | Insert(old,opos,olen) -> 
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 03ca706c8..275a730b6 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -560,8 +560,8 @@ class font_param_box param =
     let _ = dialog#connect#destroy GMain.Main.quit in
     let _ = wb_ok#connect#clicked
 	(fun () -> 
-	  let font_opt = dialog#selection#font_name in
-(*	  we#set_text (match font_opt with None -> "" | Some s -> s) ;
+(*	  let font_opt = dialog#selection#font_name in
+	  we#set_text (match font_opt with None -> "" | Some s -> s) ;
 	  set_entry_font font_opt;*)
 	  dialog#destroy ()
 	)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8faec21df..a3c2a0447 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1306,7 +1306,7 @@ let rec extern_cases_pattern_in_scope scopes vars pat =
 	
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
-  | (keyrule,pat,n as rule)::rules ->
+  | (keyrule,pat,n as _rule)::rules ->
       try
 	(* Check the number of arguments expected by the notation *)
 	let loc = match t,n with
@@ -1718,7 +1718,7 @@ and extern_numeral loc scopes (sc,n) =
 
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
-  | (keyrule,pat,n as rule)::rules ->
+  | (keyrule,pat,n as _rule)::rules ->
       let loc = Rawterm.loc_of_rawconstr t in
       try
 	(* Adjusts to the number of arguments expected by the notation *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 498c483dc..b7be8502d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -337,7 +337,7 @@ let interp_reference vars r =
   let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r 
   in r
 
-let apply_scope_env (ids,_,scopes as env) = function
+let apply_scope_env (ids,_,scopes) = function
   | [] -> (ids,None,scopes), []
   | sc::scl -> (ids,sc,scopes), scl
 
@@ -415,7 +415,7 @@ let check_or_pat_variables loc ids idsl =
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
      point and a substitution mapping extra aliases to the first one *)
-let merge_aliases (ids,subst as aliases) id =
+let merge_aliases (ids,subst as _aliases) id =
   ids@[id], if ids=[] then subst else (id, List.hd ids)::subst
 
 let alias_of = function
@@ -651,12 +651,12 @@ let merge_impargs l args =
       | _ -> a::l)
     l args 
 
-let check_projection isproj nargs r = 
+let check_projection isproj r = 
   match (r,isproj) with
   | RRef (loc, ref), Some nth ->
       (try
-	let n = Recordops.find_projection_nparams ref in
-	if nargs < nth then 
+	let n = Recordops.find_projection_nparams ref + 1 in
+	if nth < n then 
 	  user_err_loc (loc,"",str "Projection has not enough parameters");
       with Not_found -> 
 	user_err_loc
@@ -735,7 +735,7 @@ let rec subst_iterator y t = function
   | RVar (_,id) as x -> if id = y then t else x
   | x -> map_rawconstr (subst_iterator y t) x
 
-let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) =
+let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) =
   function
   | AVar id ->
       begin
@@ -801,15 +801,14 @@ let internalise sigma env allow_soapp lvar c =
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
-	let ids' = List.fold_right Idset.add lf ids in
         let idl = Array.map
           (fun (id,n,bl,ty,bd) ->
-            let ((ids'',_,_),rbl) =
+            let ((ids',_,_),rbl) =
               List.fold_left intern_local_binder (env,[]) bl in
-	    let ids''' = List.fold_right Idset.add lf ids'' in
+	    let ids'' = List.fold_right Idset.add lf ids' in
             (List.rev rbl,
-             intern_type (ids'',tmp_scope,scopes) ty,
-             intern (ids''',None,scopes) bd)) dl in
+             intern_type (ids',tmp_scope,scopes) ty,
+             intern (ids'',None,scopes) bd)) dl in
 	RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
@@ -824,15 +823,14 @@ let internalise sigma env allow_soapp lvar c =
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
 	in
-	let ids' = List.fold_right Idset.add lf ids in
         let idl = Array.map
           (fun (id,bl,ty,bd) ->
-            let ((ids'',_,_),rbl) =
+            let ((ids',_,_),rbl) =
               List.fold_left intern_local_binder (env,[]) bl in
-	    let ids''' = List.fold_right Idset.add lf ids'' in
+	    let ids'' = List.fold_right Idset.add lf ids' in
             (List.rev rbl,
-             intern_type (ids'',tmp_scope,scopes) ty,
-             intern (ids''',None,scopes) bd)) dl in
+             intern_type (ids',tmp_scope,scopes) ty,
+             intern (ids'',None,scopes) bd)) dl in
 	RRec (loc,RCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
@@ -864,7 +862,7 @@ let internalise sigma env allow_soapp lvar c =
 	intern (ids,None,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
         let (f,_,args_scopes,_) = intern_reference env lvar ref in
-	check_projection isproj (List.length args) f;
+	check_projection isproj f;
 	RApp (loc, f, intern_args env args_scopes args)
     | CApp (loc, (isproj,f), args) ->
         let isproj,f,args = match f with
@@ -879,8 +877,9 @@ let internalise sigma env allow_soapp lvar c =
                 let c = intern_notation intern env loc ntn [] in
                 find_appl_head_data lvar c
             | x -> (intern env f,[],[],[]) in
-	let args = intern_impargs c env impargs args_scopes (merge_impargs l args) in
-	check_projection isproj (List.length args) c;
+	let args = 
+	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
+	check_projection isproj c;
 	(match c with 
           (* Now compact "(f args') args" *)
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
@@ -919,7 +918,7 @@ let internalise sigma env allow_soapp lvar c =
 	RPatVar (loc, n)
     | CPatVar (loc, (false,n)) when Options.do_translate () ->
 	RVar (loc, n)
-    | CPatVar (loc, (false,n as x)) ->
+    | CPatVar (loc, (false,n)) ->
         if List.mem n (fst (let (a,_,_,_,_) = lvar in a)) & !Options.v7 then
 	  RVar (loc, n)
 	else
@@ -951,7 +950,7 @@ let internalise sigma env allow_soapp lvar c =
         ((name_fold Idset.add na ids,ts,sc),
          (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
-  and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) =
+  and intern_eqn n (ids,tmp_scope,scopes as _env) (loc,lhs,rhs) =
     let idsl_pll = List.map (intern_cases_pattern scopes ([],[]) None) lhs in
 
     let eqn_ids,pll = product_of_cases_patterns [] idsl_pll in
diff --git a/interp/genarg.ml b/interp/genarg.ml
index f81425eb8..d9afc146b 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -181,24 +181,24 @@ let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen"
 let genarg_tag (s,_) = s
 
 let fold_list0 f = function
-  | (List0ArgType t as u, l) ->
+  | (List0ArgType t, l) ->
       List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
   | _ -> failwith "Genarg: not a list0"
 
 let fold_list1 f = function
-  | (List1ArgType t as u, l) ->
+  | (List1ArgType t, l) ->
       List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
   | _ -> failwith "Genarg: not a list1"
 
 let fold_opt f a = function
-  | (OptArgType t as u, l) ->
+  | (OptArgType t, l) ->
       (match Obj.magic l with
 	| None -> a
 	| Some x -> f (in_gen t x))
   | _ -> failwith "Genarg: not a opt"
 
 let fold_pair f = function
-  | (PairArgType (t1,t2) as u, l) ->
+  | (PairArgType (t1,t2), l) ->
       let (x1,x2) = Obj.magic l in
       f (in_gen t1 x1) (in_gen t2 x2)
   | _ -> failwith "Genarg: not a pair"
diff --git a/interp/notation.ml b/interp/notation.ml
index c3903cfc1..7874f95b3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -214,8 +214,6 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
     patl
 
 let check_required_module loc sc (ref,d) =
-  let d' = List.map id_of_string d in
-  let dir = make_dirpath (List.rev d') in
   try let _ = sp_of_global ref in ()
   with Not_found ->
     user_err_loc (loc,"numeral_interpreter",
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
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 989c8f22d..4febb3ad1 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -57,7 +57,7 @@
     let rec add x data = function
         Empty ->
           Node(Empty, x, data, Empty, 1)
-      | Node(l, v, d, r, h) as t ->
+      | Node(l, v, d, r, h) ->
           let c = Pervasives.compare x v in
           if c = 0 then
             Node(l, x, data, r, h)
@@ -91,7 +91,7 @@
     let rec remove x = function
         Empty ->
           Empty
-      | Node(l, v, d, r, h) as t ->
+      | Node(l, v, d, r, h) ->
           let c = Pervasives.compare x v in
           if c = 0 then
             merge l r
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 7f0def529..91a99b5fb 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -183,7 +183,6 @@ let rec pr_com ft s =
 
 (* pretty printing functions *)
 let pp_dirs ft = 
-  let maxbox = (get_gp ft).max_depth in
   let pp_open_box = function
     | Pp_hbox n   -> Format.pp_open_hbox ft ()
     | Pp_vbox n   -> Format.pp_open_vbox ft n
diff --git a/lib/profile.ml b/lib/profile.ml
index 1197c92a9..80ae6b4b4 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -259,9 +259,9 @@ let time_overhead_B_C () =
   for i=1 to loops do
     try
       dummy_last_alloc := get_alloc ();
-      let r = dummy_f dummy_x in
-      let dw = dummy_spent_alloc () in
-      let dt = get_time () in
+      let _r = dummy_f dummy_x in
+      let _dw = dummy_spent_alloc () in
+      let _dt = get_time () in
       ()
     with _ -> assert false
   done;
diff --git a/library/declare.ml b/library/declare.ml
index 1b48acf04..bb66d3f26 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -147,7 +147,7 @@ let load_constant i ((sp,kn),(_,_,_,kind)) =
 let open_constant i ((sp,kn),_) =
   Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
 
-let cache_constant ((sp,kn),(cdt,dhyps,imps,kind) as o) =
+let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   if Idmap.mem id !vartab then
@@ -211,7 +211,7 @@ let hcons_constant_declaration = function
 
 let declare_constant_common id dhyps (cd,kind) =
   let imps = implicits_flags () in
-  let (sp,kn as oname) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
+  let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
   let kn = constant_of_kn kn in
   kn
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 69aea75f8..250411e6b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -572,7 +572,6 @@ let library_cache = Hashtbl.create 17
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
-  let prefix = dir, (mp, empty_dirpath) in
   let substobjs, objects =
     try 
       ignore(Global.lookup_module mp);
diff --git a/library/impargs.ml b/library/impargs.ml
index f41d26c99..abf583d99 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -143,7 +143,7 @@ let update pos rig (na,st) =
       | Some (DepFlexAndRigid (fpos,rpos) as x) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos else
           if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x
-      | Some (DepFlex fpos as x) ->
+      | Some (DepFlex fpos) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos
           else DepFlexAndRigid (fpos,pos)
       | Some Manual -> assert false
diff --git a/library/lib.ml b/library/lib.ml
index b8e7cea95..b1896ae5e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -50,7 +50,7 @@ let subst_objects prefix subst seg =
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
-    | ((sp,kn as oname),Leaf o) as node :: stk -> 
+    | ((sp,kn as oname),Leaf o) :: stk -> 
 	let id = id_of_label (label kn) in
 	  (match classify_object (oname,o) with 
 	     | Dispose -> clean acc stk
diff --git a/library/nametab.ml b/library/nametab.ml
index 0ce45c4fb..ddd06c0c2 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -96,7 +96,7 @@ struct
      [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
 
   let rec push_until uname o level (current,dirmap) = function
-    | modid :: path as dir ->
+    | modid :: path ->
 	let mc = 
 	  try ModIdmap.find modid dirmap
 	  with Not_found -> (Nothing, ModIdmap.empty)
@@ -135,7 +135,7 @@ struct
 
 
 let rec push_exactly uname o level (current,dirmap) = function
-  | modid :: path as dir ->
+  | modid :: path ->
       let mc = 
 	try ModIdmap.find modid dirmap
 	with Not_found -> (Nothing, ModIdmap.empty)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index c0207f077..059a93571 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -165,7 +165,6 @@ let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl =
 
 let declare_vernac_argument for_v8 loc s cl =
   let se = mlexpr_of_string s in
-  let typ = ExtraArgType s in
   let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
   <:str_item<
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 82e651b4e..f78373c28 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -127,8 +127,6 @@ let inside_printer posneg std_pr p =
 	let pr = if posneg then pr_pos else pr_neg in
 	str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")"
 in
-let outside_zero_printer std_pr p = str "`0`"
-in
 let outside_printer posneg std_pr p =
   let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in
   match (bignat_option_of_pos xI xO xH p) with
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c016d86f7..1534123f8 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -293,14 +293,14 @@ let rec comment bp = parser bp2
        s >] -> comment bp s
   | [< ''*';
        _ = parser
-         | [< '')' >] ep -> push_string "*)";
+         | [< '')' >] -> push_string "*)";
          | [< s >] -> real_push_char '*'; comment bp s >] -> ()
   | [< ''"'; s >] ->
       if Options.do_translate() then (push_string"\"";comm_string bp2 s)
       else ignore (string bp2 0 s);
       comment bp s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
-  | [< '_ as z; s >] ep -> real_push_char z; comment bp s
+  | [< '_ as z; s >] -> real_push_char z; comment bp s
 
 (* Parse a special token, using the [token_tree] *)
 
@@ -370,7 +370,7 @@ let parse_after_dot bp c strm =
 	   len = ident_tail (store (store 0 c1) c2) >] ->
 	     ("FIELD", get_buff len)
          (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
-	 | [< ''\226' as c1; t = parse_226_tail 
+	 | [< ''\226'; t = parse_226_tail 
 	     (progress_special '.' (Some !token_tree)) >] ep ->
 	     (match t with
 	       | TokSymbol (Some t) -> ("", t)
@@ -391,7 +391,7 @@ let parse_after_dot bp c strm =
 	   len = ident_tail (store (store 0 c1) c2) >] ->
 	     ("FIELD", get_buff len)
          (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
-	 | [< ''\226' as c1; t = parse_226_tail 
+	 | [< ''\226'; t = parse_226_tail 
 	     (progress_special '.' (Some !token_tree)) >] ep ->
 	     (match t with
 	       | TokSymbol (Some t) -> ("", t)
@@ -403,7 +403,7 @@ let parse_after_dot bp c strm =
 (* Parse a token in a char stream *)
 
 let rec next_token = parser bp
-  | [< '' ' | '\t' | '\n' |'\r' as c; s >] ep ->
+  | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
       comm_loc bp; push_char c; next_token s
   | [< ''$'; len = ident_tail (store 0 '$') >] ep -> 
       comment_stop bp;
@@ -424,7 +424,7 @@ let rec next_token = parser bp
       comment_stop bp;
       (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
   (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
-  | [< ''\226' as c1; t = parse_226_tail (Some !token_tree) >] ep ->
+  | [< ''\226'; t = parse_226_tail (Some !token_tree) >] ep ->
       comment_stop bp;
       (match t with
 	| TokSymbol (Some t) -> ("", t), (bp, ep)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 292e981be..90e93b832 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -629,7 +629,7 @@ let find_position forpat other assoc lev =
 	    (* Maybe this was (p,Left) and p occurs a second time *)
 	    if a = Gramext.LeftA then
 	      match l with
-		| (p,a)::_ as l' when p = n -> raise (Found a)
+		| (p,a)::_ when p = n -> raise (Found a)
 		| _ -> after := Some pa; pa::(n,create_assoc assoc)::l
 	    else
 	      (* This was not (p,LeftA) hence assoc is RightA *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 0dc646198..29501d2a1 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -422,10 +422,8 @@ let pr_extend_gen prgen lev s l =
 let make_pr_tac (pr_tac_level,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
 
 let pr_bindings = pr_bindings pr_constr pr_constr in
-let pr_bindings_no_with = pr_bindings_no_with pr_constr pr_constr in
 let pr_with_bindings = pr_with_bindings pr_constr pr_constr in
 let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in
-let pr_constrarg c = spc () ++ pr_constr c in
 let pr_intarg n = spc () ++ int n in
 
   (* Printing tactics as arguments *)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 97139ec15..13d6a62b4 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -495,9 +495,7 @@ let print_name ref =
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object")
 
 let print_opaque_name qid = 
-  let sigma = Evd.empty in
   let env = Global.env () in
-  let sign = Global.named_context () in
   match global qid with
     | ConstRef cst ->
 	let cb = Global.lookup_constant cst in
@@ -515,7 +513,6 @@ let print_opaque_name qid =
 	print_named_decl (id,c,ty)
 
 let print_about ref = 
-  let sigma = Evd.empty in
   let k = locate_any_name ref in
   begin match k with
   | Term ref -> 
diff --git a/parsing/search.ml b/parsing/search.ml
index 84022e7b1..ec7db4889 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -48,7 +48,6 @@ let rec head_const c = match kind_of_term c with
 
 let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
-  let imported = Library.opened_libraries() in
   let crible_rec (sp,_) lobj = match object_tag lobj with
     | "VARIABLE" ->
 	(try 
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 21b96c8a7..a8e47aa9b 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -140,17 +140,6 @@ let new_tac_ext (s,cl) =
 let declare_tactic_v7 loc s cl =
   let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
-  let hide_tac (_,p,e) =
-    (* reste a definir les fonctions cachees avec des noms frais *)
-    let stac = let s = "h_"^s in s.[2] <- Char.lowercase s.[2]; s in
-    let e = 
-      make_fun
-        <:expr<
-          Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$
-        >>
-      p in
-    <:str_item< value $lid:stac$ = $e$ >>
-  in
   let se = mlexpr_of_string s in
   <:str_item<
     declare
@@ -194,7 +183,6 @@ let declare_tactic loc s cl =
     <:str_item< value $lid:stac$ = $e$ >>
   in
   let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in
-  let se = mlexpr_of_string s in
   let atomic_tactics =
     mlexpr_of_list mlexpr_of_string
       (List.flatten (List.map (fun (al,_) -> is_atomic al) cl')) in
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 6063e9448..942bce798 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -94,7 +94,6 @@ let rec print_script nochange sigma osign pf =
 (* printed by Show Script command *)
 let print_treescript nochange sigma _osign pf =
   let rec aux top pf =
-    let {evar_hyps=sign; evar_concl=cl} = pf.goal in
     match pf.ref with
     | None ->
         if nochange then 
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"
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 303338143..3db11ce39 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -30,7 +30,6 @@ let w_refine env ev rawc evd =
   let sigma,typed_c = 
     Pretyping.understand_gen_tcc (evars_of evd) env [] 
       (Some e_info.evar_concl) rawc in
-  let inst_info = {e_info with evar_body = Evar_defined typed_c } in
   evar_define ev typed_c (evars_reset_evd sigma evd)
 
 (* vernac command Existential *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6da2c8c2f..8e02a7b27 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -79,7 +79,7 @@ let make_flag f =
   in red
 
 let is_reference c = 
-  try let r = global_of_constr c in true with _ -> false
+  try let _ref = global_of_constr c in true with _ -> false
 
 let red_expr_tab = ref Stringmap.empty
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 37dc016c9..816fdf932 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -217,7 +217,7 @@ let mutual_cofix f others gl =
   with_check (refiner (Prim (Cofix (f,others)))) gl
     
 let rename_bound_var_goal gls =
-  let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in 
+  let { evar_hyps = sign; evar_concl = cl } = sig_it gls in 
   let ids = ids_of_named_context sign in
   convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls
 
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 3808cbe10..784bbdc3d 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -198,7 +198,6 @@ let clean file =
 let all_modules_in_dir dir =
   try
     let lst = ref []
-    and stg = ref ""
     and dh = Unix.opendir dir in
     try
       while true do
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 = 
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 88983637a..eb767694b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -268,8 +268,6 @@ lorque source est None alors target est None aussi.
 
 let add_new_coercion_core coef stre source target isid =
   check_source source;
-  let env = Global.env () in
-  let v = constr_of_global coef in
   let t = Global.type_of_global coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let tg,lp = prods_of t in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2da3e2cf5..0a97baf8b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -171,7 +171,7 @@ let assumption_message id =
 let declare_one_assumption is_coe (local,kind) c (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
-        let r = 
+        let _ = 
           declare_variable ident 
             (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in
         assumption_message ident;
@@ -279,8 +279,7 @@ let interp_mutual lparams lnamearconstrs finite =
       [] lnamearconstrs in
   if not (list_distinct allnames) then
     error "Two inductive objects have the same name";
-  let nparams = local_binders_length lparams
-  and sigma = Evd.empty 
+  let sigma = Evd.empty 
   and env0 = Global.env() in
   let env_params, params =
     List.fold_left
@@ -313,8 +312,6 @@ let interp_mutual lparams lnamearconstrs finite =
   let paramassums = 
     List.fold_right (fun d l -> match d with
 	(id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in
-  let indnames =
-    List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
   let nparamassums = List.length paramassums in
   let (ind_env,ind_impls,arityl) =
     List.fold_left
@@ -432,7 +429,7 @@ let extract_coe_la_lc = function
 let build_mutual lind finite =
   let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in
   let notations,mie = interp_mutual lparams lnamearconstructs finite in
-  let kn = declare_mutual_with_eliminations false mie in
+  let _ = declare_mutual_with_eliminations false mie in
   (* Declare the notations now bound to the inductive types *)
   List.iter (fun (df,c,scope) ->
     Metasyntax.add_notation_interpretation df [] c scope) notations;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cc3740501..56f6b111e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -129,7 +129,6 @@ let re_exec is_ide =
   let s = !re_exec_version in
   let is_native = (Mltop.get()) = Mltop.Native in
   let prog = Sys.argv.(0) in
-  let coq = Filename.basename prog in
   if (is_native && s = "byte") || ((not is_native) && s = "opt")
   then begin
     let s = if s = "" then if is_native then "opt" else "byte" else s in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8b72d5b01..55201ea43 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -84,7 +84,6 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
   let ctx = make_all_name_different ctx in
   let pi = pr_inductive ctx ind in
   let pc = prterm_env ctx c in
-  let ppt = prterm_env ctx pj.uj_type in
   let msg = match okinds with
   | Some(kp,ki,explanation) ->
       let pki = prterm_env ctx ki in
@@ -380,7 +379,6 @@ let explain_var_not_found ctx id =
   spc ()  ++ str "in the current" ++ spc ()  ++ str "environment"
 
 let explain_wrong_case_info ctx ind ci =
-  let ctx = make_all_name_different ctx in
   let pi = prterm (mkInd ind) in
   if ci.ci_ind = ind then
     str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++
@@ -646,8 +644,8 @@ let explain_needs_inversion ctx x t =
   px  ++ str " of type: " ++ pt
 
 let explain_unused_clause env pats =
-  let s = if List.length pats > 1 then "s" else "" in
 (* Without localisation
+  let s = if List.length pats > 1 then "s" else "" in
   (str ("Unused clause with pattern"^s) ++ spc () ++
     hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
 *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a99a15b35..498b21f7f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -201,7 +201,6 @@ let check_entry_type (u,n) =
     | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
 
 let add_grammar_obj univ entryl =
-  let u = create_univ_if_new univ in
   let g = interp_grammar_command univ check_entry_type entryl in
   Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g))
 
@@ -662,12 +661,12 @@ let read_recursive_format sl fmt =
   let slfmt, fmt = get_head fmt in
   slfmt, get_tail (slfmt, fmt)
 
-let hunks_of_format (from,(vars,typs) as vt) symfmt = 
+let hunks_of_format (from,(vars,typs)) symfmt = 
   let rec aux = function
   | symbs, (UnpTerminal s' as u) :: fmt
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
-  | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt
+  | Terminal s :: symbs, (UnpTerminal s') :: fmt
       when s = unquote_notation_token s' ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
@@ -811,7 +810,6 @@ let pr_arg_level from = function
   | (n,_) -> str "Unknown level"
 
 let pr_level ntn (from,args) =
-  let lopen = ntn.[0] = '_' and ropen = ntn.[String.length ntn - 1] = '_' in
 (*
   let ppassoc, args = match args with
     | [] -> mt (), []
@@ -1350,7 +1348,6 @@ let add_notation local c dfmod mv8 sc =
                   add_notation_in_scope local df c modifiers mv8 sc toks
 	  | Some n ->
 	    (* Declare both syntax and interpretation *)
-	    let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
             add_notation_in_scope local df c modifiers mv8 sc toks
 
 (* TODO add boxes information in the expression *)
@@ -1410,7 +1407,6 @@ let add_infix local (inf,modl) pr mv8 sc =
       let (recs,vars,symbs) = analyse_notation_tokens toks in
       let (acvars,ac) = interp_aconstr [] vars a in
       let a' = (remove_vars recs acvars,ac) in
-      let a_for_old = interp_global_rawconstr_with_vars vars a in
       add_notation_interpretation_core local symbs None df a' sc 
 	onlyparse true None
     else
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 926d3e73b..124ad03c6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -64,7 +64,6 @@ let cl_of_qualid = function
 
 let show_proof () =
   let pts = get_pftreestate () in
-  let pf = proof_of_pftreestate pts in
   let cursor = cursor_of_pftreestate pts in
   let evc = evc_of_pftreestate pts in
   let (pfterm,meta_types) = extract_open_pftreestate pts in
@@ -1096,8 +1095,7 @@ let vernac_show = function
 
 let vernac_check_guard () =
   let pts = get_pftreestate () in
-  let pf = proof_of_pftreestate pts 
-  and cursor = cursor_of_pftreestate pts in
+  let pf = proof_of_pftreestate pts in
   let (pfterm,_) = extract_open_pftreestate pts in
   let message = 
     try 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index e5d7d75bd..a8d0b1390 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -211,9 +211,6 @@ let pr_opt_hintbases l = match l with
 
 let pr_hints local db h pr_c pr_pat = 
   let opth = pr_opt_hintbases db  in
-  let pr_aux = function
-    | CAppExpl (_,(_,qid),[]) -> pr_reference qid
-    | _ -> mt () in
   let pph =
     match h with
     | HintsResolve l ->
@@ -604,8 +601,6 @@ let rec pr_vernac = function
             str"Eval" ++ spc() ++
             pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++
             str" in" ++ spc() in
-      let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) in
-      let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) in
       let pr_def_body = function
         | DefineBody (bl,red,c,d) ->
             let (bl2,body,ty) = match d with
@@ -654,8 +649,7 @@ let rec pr_vernac = function
       (* Copie simplifiée de command.ml pour recalculer les implicites, *)
       (* les notations, et le contexte d'evaluation *)
       let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in
-      let nparams = local_binders_length lparams
-      and sigma = Evd.empty 
+      let sigma = Evd.empty 
       and env0 = Global.env() in
       let (env_params,params) =
 	List.fold_left
@@ -684,12 +678,10 @@ let rec pr_vernac = function
 	    (env', (recname,impls)::ind_impls, (arity::arl)))
           (env0, [], []) l
       in
-      let lparnames = List.map (fun (na,_,_) -> na) params in
       let notations = 
 	List.fold_right (fun (_,ntnopt,_,_,_) l ->option_cons ntnopt l) l [] in
       let ind_env_params = Environ.push_rel_context params ind_env in
 
-      let lparnames = List.map (fun (na,_,_) -> na) params in
       let impl = List.map
 	(fun ((_,recname),_,_,arityc,_) ->
 	  let arity = Constrintern.interp_type sigma env_params arityc in