From 7a0b94914c466d8167497f5d3df42759d78093f9 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Feb 2004 14:11:01 +0000
Subject: [PATCH] - the result of a refinement is now cleared from dummy
 dependent types   and letins - freshNameGenerator: bug fixed

---
 helm/ocaml/cic_unification/cicRefine.ml       | 41 ++++++++++++++++---
 .../cic_unification/freshNamesGenerator.ml    |  2 +-
 2 files changed, 37 insertions(+), 6 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 85c171b14..c9c8f4d82 100644
--- 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 *)
diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 3664b4a72..80a26888f 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -69,7 +69,7 @@ let clean_dummy_dependent_types t =
  let module C = Cic in
   let rec aux k =
    function
-      C.Rel m as t -> t,[m - k]
+      C.Rel m as t -> t,[k - m]
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst',rels = 
         List.fold_right
-- 
2.39.2