- 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 85c171b14973704f524451621f21847d1eb17c12..c9c8f4d8256184569ea8662a2416b3aeaefc74e3 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -532,11 +532,42 @@ and type_of_aux' metasenv context t =
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
   in
-   (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')
+   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 *)