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))
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