- m1', m2', (m1' == m1 && m2' == m2) || delta = 0
- (* if we have as heads two Fix of height n>0, they may or may not
- * reduce, depending on their rec argument... we thus check if
- * something changed or not. This relies on the reduction machine
- * preserving the original machine if it performs no action *)
+ if (m1' == m1 && m2' == m2 && delta > 0) then
+ (* if we have as heads a Fix of height n>m>0 and another term of height
+ * m, we set delta = m. The Fix may or may not reduce, depending on its
+ * rec argument. if no reduction was performed we decrease delta to m-1
+ * to reduce the other term *)
+ let delta = delta - 1 in
+ pp ("DELTA STEP TO: " ^ string_of_int delta);
+ let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+ let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+ m1', m2', (m1 == m1' && m2 == m2') || delta = 0
+ else m1', m2', delta = 0