Bug fixed: the domain of a LetRec was only made by the last function in the

[helm.git] / helm / software / components / ng_kernel / nCicReduction.ml

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 118bc6911ad9e1149a66887b871074fd85a5ac07..46a81d6205417451d5ed611a35f4cf75f2d52e86 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -401,7 +401,7 @@ module Reduction(RS : Strategy) =
          if delta > height then config else aux (0, [], body, s) 
      | (_, _, NCic.Const (NReference.Ref 
                (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
-        let fixes,_, height = NCicEnvironment.get_checked_fixes refer in
+        let fixes,_, height = NCicEnvironment.get_checked_fixes_or_cofixes refer in
         if delta > height then config else
         (match
           try Some (RS.from_stack (List.nth s recindex))
@@ -421,7 +421,7 @@ module Reduction(RS : Strategy) =
      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
         let decofix = function
           | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
-             let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in
+             let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
              let _,_,_,_,body = List.nth cofixes c in
              reduce ~delta:0 ~subst context (0,[],body,s)
           | config -> config