X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=95e6c7ba6d213ef308592031b32e4e550666d29a;hb=b52f57d8573a909a486d52a7317e017f56d07199;hp=20be9363bbbc385ad82d972ad51b1769635bc4b1;hpb=db7935f343aa2cb11bd3f8ee5c56112e2e266cd3;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 20be9363b..95e6c7ba6 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1331,7 +1331,9 @@ let typecheck metasenv uri obj ~localization_tbl =
          let metasenv,ugraph,cl' =
           List.fold_right
            (fun (name,ty) (metasenv,ugraph,res) ->
-             let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+             let ty =
+              CicTypeChecker.debrujin_constructor
+               ~cb:(relocalize localization_tbl) uri typesno ty in
              let ty',_,metasenv,ugraph =
               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in