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

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index defd12e29..db19c9c96 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -421,8 +421,8 @@ module Reduction(RS : Strategy) =
          let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
          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
+               (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
+        let fixes,_, height = NCicEnvironment.get_checked_fixes refer in
         if delta > height then config else
         (match
           try Some (RS.from_stack (List.nth s recindex))
@@ -435,13 +435,15 @@ module Reduction(RS : Strategy) =
                let new_s =
                  replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
                in
+               let _,_,_,_,body = List.nth fixes fixno in
                aux (0, [], body, new_s)
            | _ -> config)
      | (_, _, NCic.Const _, _) as config -> config
      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
         let decofix = function
-          | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix _)as refer),s)->
-             let _,_,body,_,_,_ = NCicEnvironment.get_checked_cofix refer in
+          | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
+             let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in
+             let _,_,_,_,body = List.nth cofixes c in
              reduce ~delta:0 ~subst context (0,[],body,s)
           | config -> config
         in