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 7fa80b5bbc46852f604f7a547f1b064dbfdf16e2..71c104be73301a2887b7451491cf4bc7bb2dca6b 100644 (file)
--- 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