new calculation of recursive parameters in guarded by destructors:

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index dd5191a156543b59148d15ff261938f7548425e2..065dbc33d9cd8a3e2d6a6a175962809e63a9997e 100644 (file)
--- 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