X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_extraction%2Fextraction.ml;h=be8099598e31eb5e804d482cb0c270518ffae94b;hb=3df31c02806eca83c63c14e6a89844f764c3e2cb;hp=382801b617203c6a9de903c2f5ab1f2e7af667cc;hpb=e2718488c73b2cdf20b26af46e80a11b91fac220;p=helm.git

diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml
index 382801b61..be8099598 100644
--- a/matita/components/ng_extraction/extraction.ml
+++ b/matita/components/ng_extraction/extraction.ml
@@ -207,7 +207,7 @@ let sign_with_implicits _r s =
 
 (* Enriching a exception message *)
 
-let rec handle_exn _r _n _fn_name = function x -> x
+let handle_exn _r _n _fn_name = function x -> x
 (*CSC: only for pretty printing
   | MLexn s ->
       (try Scanf.sscanf s "UNBOUND %d"
@@ -1014,7 +1014,7 @@ and extract_case context mle (ip,c,br) status 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 status context c t =
+let decomp_lams_eta_n n m status context c t =
   let rels = fst (splay_prod_n status context n t) in
   let rels',c = decompose_lam c in
   let d = n - m in