- the result of a refinement is now cleared from dummy dependent types

[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..c9c8f4d8256184569ea8662a2416b3aeaefc74e3 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,9 +532,42 @@ 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,
-    CicMetaSubst.apply_subst_metasenv subst' metasenv')
+   let substituted_t = CicMetaSubst.apply_subst subst' t in
+   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
+   let substituted_metasenv =
+    CicMetaSubst.apply_subst_metasenv subst' metasenv'
+   in
+    let cleaned_t =
+     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+    let cleaned_ty =
+     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+    let cleaned_metasenv =
+     List.map
+      (function (n,context,ty) ->
+        let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
+        let context' =
+         List.map
+          (function
+              None -> None
+            | Some (n, Cic.Decl t) ->
+               Some (n,
+                Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
+            | Some (n, Cic.Def (bo,ty)) ->
+               let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
+               let ty' =
+                match ty with
+                   None -> None
+                 | Some ty ->
+                    Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+               in
+                Some (n, Cic.Def (bo',ty'))
+          ) context
+        in
+         (n,context',ty')
+      ) substituted_metasenv
+    in
+     (cleaned_t,cleaned_ty,cleaned_metasenv)
+
 ;;
 
 (* DEBUGGING ONLY *)