X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=07eba73b564385b6742ada4848bcb16be7f255fd;hb=9aaaba04fbd198881aaee42cfc41fdb75db1eeaa;hp=fc6eea759313223b30c57a7b6215470ea12c24d5;hpb=c6ec0dc44c2e592c7b1323304052bc1a523e7c22;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index fc6eea759..07eba73b5 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -623,8 +623,8 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
             | _ -> [] *) in
           let unif_from_stack t1 t2 b metasenv subst =
               try
-                let t1 = NCicReduction.from_stack t1 in
-                let t2 = NCicReduction.from_stack t2 in
+                let t1 = NCicReduction.from_stack ~delta:max_int t1 in
+                let t2 = NCicReduction.from_stack ~delta:max_int t2 in
                 unif_machines metasenv subst (put_in_whd t1 t2)
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst