X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.ml;h=08cb06d9d93b8dcc49a827223fd1b2d7e629c01c;hb=200d1d63cd5fc282df768f97d33214c1572c89da;hp=1861ce5b0222e132d53d72f08474f471f6bbbbfc;hpb=756c1e676368d9addc75438bce97a71e34287f18;p=helm.git

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 1861ce5b0..08cb06d9d 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -75,7 +75,9 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
 (*CSC: type-inference, but the result is very poort. As a very weak   *)
 (*CSC: patch, I apply whd to the computed type. Full beta             *)
 (*CSC: reduction would be a much better option.                       *)
-        let innertype = CicReduction.whd (T.type_of_aux' metasenv cicenv tt) in
+        let innertype =
+         CicReduction.whd cicenv (T.type_of_aux' metasenv cicenv tt)
+        in
          let innersort = T.type_of_aux' metasenv cicenv innertype in
           let ainnertype =
            if computeinnertypes then