* 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 239db16cf11560a552531c03ee2aebe83fa2be1d..6d28ca1779972be28c6619ad7f0cd5bed8be78b5 100644 (file)
--- 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 -