Experimental commit: definitions are now allowed in contexts. As a consequence,

[helm.git] / helm / gTopLevel / cic2acic.ml

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 1861ce5b0222e132d53d72f08474f471f6bbbbfc..08cb06d9d93b8dcc49a827223fd1b2d7e629c01c 100644 (file)
--- 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