- let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
- let h1, flex1 = height_of is_whd t1 in
- let h2, flex2 = height_of is_whd t2 in
+ let put_in_whd m1 m2 =
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m2
+ in
+ let small_delta_step
+ ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
+ =
+ assert (not (norm1 && norm2));
+ if norm1 then
+ x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
+ else if norm2 then
+ NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
+ else
+ let h1 = height_of t1 in
+ let h2 = height_of t2 in