5 files changed, 5 insertions, 8 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 359257c88..750729660 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -310,7 +310,6 @@ module StdParams = struct
 	(*i TODO: clash possible i*)
 	list_firstn ((mp_length mp)-(mp_length pref)) ls
       with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
-	let base = base_mp mp in 
 	if !modular && (at_toplevel mp) 
 	then snd (list_sep_last ls)
 	else ls
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 55ad52ee2..16d85a3f9 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -230,7 +230,7 @@ let rec extract_type env db j c args =
 		      (* We try to reduce. *)
 		      let newc = applist (Declarations.force lbody, args) in 
 		      extract_type env db j newc []))
-    | Ind ((kn,i) as ip) ->
+    | Ind (kn,i) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in  
 	extract_type_app env db (IndRef (kn,i),s) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
@@ -676,7 +676,6 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
       end 
     else 
       let mi = extract_ind env kn in 
-      let params_nb = mi.ind_nparams in 
       let oi = mi.ind_packets.(i) in 
       let metas = Array.init (List.length oi.ip_vars) new_meta in 
       (* The extraction of the head. *)
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 5c842f159..b909eead5 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -256,7 +256,7 @@ type abbrev_map = global_reference -> ml_type option
 let type_expand env t = 
   let rec expand = function
     | Tmeta {contents = Some t} -> expand t
-    | Tglob (r,l) as t ->    
+    | Tglob (r,l) ->    
 	(match env r with 
 	   | Some mlt -> expand (type_subst_list l mlt) 
 	   | None -> Tglob (r, List.map expand l))
@@ -378,7 +378,7 @@ let ast_iter f = function
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (_,c,l) -> List.iter f l
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom  -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 673c8e929..6dcfaf2a1 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -185,7 +185,7 @@ let ast_iter_references do_term do_cons do_type a =
       | MLcons (i,r,_) -> 
 	  if lang () = Ocaml then record_iter_references do_term i; 
 	  do_cons r 
-      | MLcase (i,_,v) as a -> 
+      | MLcase (i,_,v) -> 
 	  if lang () = Ocaml then record_iter_references do_term i; 
 	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f9b91d226..ee53bd49a 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -264,7 +264,6 @@ let rec pp_expr par env args =
 	let tuple = pp_tuple (pp_expr true env []) args' in 
 	pp_par par (pp_global r ++ spc () ++ tuple)
     | MLcase (i, t, pv) ->
-	let r,_,_ = pv.(0) in 
 	let expr = if i = Coinductive then 
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
 	else 
@@ -480,7 +479,7 @@ let pp_mind kn i =
 let pp_decl mpl = 
   local_mpl := mpl; 
   function
-    | Dind (kn,i) as d -> pp_mind kn i
+    | Dind (kn,i) -> pp_mind kn i
     | Dtype (r, l, t) ->
 	if is_inline_custom r then failwith "empty phrase"
 	else