From a38c7053c367734f60dd971de1fe17295271dae6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Mar 2013 01:31:00 +0000 Subject: [PATCH] Bug fixed: let-rec defined propositions are no longer extracted. They used to be extracted, but in the interface the type abstraction was wrong. --- matita/components/ng_extraction/extraction.ml | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml index 71c104be7..382801b61 100644 --- a/matita/components/ng_extraction/extraction.ml +++ b/matita/components/ng_extraction/extraction.ml @@ -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,7 +1164,8 @@ 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 _ -> + 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)) @@ -1186,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 @@ -1267,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=[]); -- 2.39.2