Merge remote-tracking branch 'origin/ld-0.99.3'

[helm.git] / matita / components / ng_extraction / extraction.ml

diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml
index 7fa80b5bbc46852f604f7a547f1b064dbfdf16e2..be8099598e31eb5e804d482cb0c270518ffae94b 100644 (file)
--- 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
@@ -1142,6 +1142,13 @@ let extract_fixpoint_common uri height fix_or_cofix ifl =
        NReference.reference_of_spec uri (NReference.CoFix i)) in
   ti,ci,n,vkn
 
+(*s Is a [ml_spec] logical ? *)
+let logical_spec = function
+  | Stype (_, [], Some (Tdummy _)) -> true
+  | Sval (_,Tdummy _) -> true
+  | Sind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+  | _ -> false
+
 let extract_fixpoint status uri height fix_or_cofix is_projection ifl =
   let status =
    if is_projection then
@@ -1157,10 +1164,10 @@ let extract_fixpoint status uri height fix_or_cofix is_projection ifl =
    (fun status i _ ->
      let _,head = split_all_prods status ~subst:[] [] ti.(i) in
      match head with
-        NCic.Sort _ ->
-         (*let n = type_scheme_nb_args status [] typ in*)
-         (*let ids = iterate (fun l -> anonymous_name::l) n [] in*)
-         let ids = [] in
+        NCic.Sort s when classify_sort s = InProp -> status,`None
+      | NCic.Sort _ ->
+         let n = type_scheme_nb_args status [] ti.(i) in
+         let ids = iterate (fun l -> anonymous_name::l) n [] in
          status,`Type (Dtype (vkn.(i), ids, Tunknown))
       | _ ->
         if sort_of status [] ti.(i) <> InProp then
@@ -1187,7 +1194,7 @@ let extract_fixpoint_spec status uri height fix_or_cofix ifl =
     (fun status i vkn ->
       if sort_of status [] ti.(i) <> InProp then begin
        let status,spec = extract_constant_spec status vkn None ti.(i) in
-       status, Some spec
+       status, if logical_spec spec then None else Some spec
       end
      else status,None
     ) vkn in
@@ -1268,14 +1275,6 @@ let logical_decl = function
   | Dind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
-(*s Is a [ml_spec] logical ? *)
-
-let logical_spec = function
-  | Stype (_, [], Some (Tdummy _)) -> true
-  | Sval (_,Tdummy _) -> true
-  | Sind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
-  | _ -> false
-
 let extract_impl status (uri,height,metasenv,subst,obj_kind) =
  assert (metasenv=[]);
  assert (subst=[]);