From d208b69293abef9a36eb5366d93f6e1ef4c8125e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 27 Feb 2013 20:17:41 +0000 Subject: [PATCH] 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. --- matita/components/ng_extraction/extraction.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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 -- 2.39.2