4 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 82a6c39336..ab0e480f9a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -72,7 +72,7 @@ type flag = info * scheme
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
-let rec flag_of_type env t =
+let rec flag_of_type env t : flag =
   let t = whd_betadeltaiota env none t in
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
@@ -844,7 +844,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_lams_eta_n n m env c t =
+let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
   let rels = List.map (fun (id,_,c) -> (id,c)) rels in
   let rels',c = decompose_lam c in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 321af2946a..a8c9375b18 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -800,7 +800,7 @@ let rec merge_ids ids ids' = match ids,ids' with
 
 let is_exn = function MLexn _ -> true | _ -> false
 
-let rec permut_case_fun br acc =
+let permut_case_fun br acc =
   let nb = ref max_int in
   Array.iter (fun (_,_,t) ->
 		let ids, c = collect_lams t in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 3d21fc2d8a..067c417056 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -120,7 +120,7 @@ let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type par vl t =
+let pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 1fd4840feb..2dd07b2f2b 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -67,7 +67,7 @@ let is_toplevel mp =
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
-let rec mp_length mp =
+let mp_length mp =
   let mp0 = current_toplevel () in
   let rec len = function
     | mp when mp = mp0 -> 1