From: Claudio Sacerdoti Coen Date: Wed, 27 Feb 2013 20:17:41 +0000 (+0000) Subject: Bug fixed that reveals a new one: in case of inductive types defined via X-Git-Tag: make_still_working~1242 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d208b69293abef9a36eb5366d93f6e1ef4c8125e Bug fixed that reveals a new one: in case of inductive types defined via let rec, it used to happen that a "type 'a foo" in the .mli was implemented by a "type 'a foo" in the .ml. Now the opposite happens in other situations. --- diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml index 7fa80b5bb..71c104be7 100644 --- a/matita/components/ng_extraction/extraction.ml +++ b/matita/components/ng_extraction/extraction.ml @@ -1158,9 +1158,8 @@ let extract_fixpoint status uri height fix_or_cofix is_projection ifl = 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 + 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