X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=defd12e292c0836dd15afb2331b070c0bac0c9f8;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=64133384d5f9a511efa91439f8e3ae970bb53f64;hpb=f4b01f86f36f3b1ee11f383e3c056a458a76cb96;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 64133384d..defd12e29 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -419,11 +419,11 @@ module Reduction(RS : Strategy) =
      | (_, _, NCic.Const
             (NReference.Ref (_,_,NReference.Def) as refer), s) as config ->
          let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
-         if delta >= height then config else aux (0, [], body, s) 
+         if delta > height then config else aux (0, [], body, s) 
      | (_, _, NCic.Const (NReference.Ref 
                (_,_,NReference.Fix (_,recindex)) as refer),s) as config ->
         let _,_,body,_, _, height = NCicEnvironment.get_checked_fix refer in
-        if delta >= height then config else
+        if delta > height then config else
         (match
           try Some (RS.from_stack (List.nth s recindex))
           with Failure _ -> None