From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 26 Nov 2005 18:05:10 +0000 (+0000)
Subject: * wrong comments removed
X-Git-Tag: make_still_working~8084
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e674cb67c1f52747111fa3935d1523e1af8222f5;p=helm.git

* wrong comments removed
* relocalization of refined terms is now performed for every refined term
---

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 239db16cf..6d28ca177 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -207,7 +207,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     let module C = Cic in
     let module S = CicSubstitution in
     let module U = UriManager in
-    (* this stops on binders, so we have to call it every time *)
+     let (t',_,_,_,_) as res =
       match t with
           (*    function *)
           C.Rel n ->
@@ -392,7 +392,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    let x',ty,subst',metasenv',ugraph1 =
                      type_of_aux subst metasenv context x ugraph
                    in
-                    relocalize localization_tbl x x';
                     (x', ty)::res,subst',metasenv',ugraph1
                 ) tl ([],subst',metasenv',ugraph1)
             in
@@ -783,6 +782,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               fl_ty' fl_bo' fl 
             in
               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
+     in
+      relocalize localization_tbl t t';
+      res
 
   (* check_metasenv_consistency checks that the "canonical" context of a
      metavariable is consitent - up to relocation via the relocation list l -