X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_extraction%2Fextraction.ml;h=71c104be73301a2887b7451491cf4bc7bb2dca6b;hb=d208b69293abef9a36eb5366d93f6e1ef4c8125e;hp=7fa80b5bbc46852f604f7a547f1b064dbfdf16e2;hpb=c5fe1eeb2b575d1c696ca15ad9155223839d82e2;p=helm.git

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