X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=065dbc33d9cd8a3e2d6a6a175962809e63a9997e;hb=97b18234921aec71a8b89ec2c1b058e12e5e043c;hp=dd5191a156543b59148d15ff261938f7548425e2;hpb=998a7855d00bcb55525a82138a3bfb4183d99014;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index dd5191a15..065dbc33d 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1942,7 +1942,7 @@ let typecheck metasenv uri obj ~localization_tbl =
            (fun (name,ty) (metasenv,ugraph,res) ->
              let ty =
               CicTypeChecker.debrujin_constructor
-               ~cb:(relocalize localization_tbl) uri typesno ty in
+              ~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