dummy dependent types and dummy letins are now removed from the refined

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 060d2bd1f767c9767fdd1c6cb99b65d22f8bca9e..85c171b14973704f524451621f21847d1eb17c12 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -511,7 +511,14 @@ and type_of_aux' metasenv context t =
             context)
        in
        let newmeta = Cic.Meta (idx, irl) in
-       let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
+       let prod =
+        Cic.Prod
+         (FreshNamesGenerator.mk_fresh_name
+           (CicMetaSubst.apply_subst_metasenv subst metasenv)
+           (CicMetaSubst.apply_subst_context subst context)
+           Cic.Anonymous
+           (CicMetaSubst.apply_subst subst argty),
+          argty, newmeta) in
        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
        let (subst, metasenv) =
          CicUnification.fo_unif_subst subst context metasenv resty prod
@@ -525,8 +532,10 @@ and type_of_aux' metasenv context t =
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
   in
-   (CicMetaSubst.apply_subst subst' t,
-    CicMetaSubst.apply_subst subst' ty,
+   (FreshNamesGenerator.clean_dummy_dependent_types
+     (CicMetaSubst.apply_subst subst' t),
+    FreshNamesGenerator.clean_dummy_dependent_types
+     (CicMetaSubst.apply_subst subst' ty),
     CicMetaSubst.apply_subst_metasenv subst' metasenv')
 ;;