else
(* we reindex the equation from scratch *)
let unit_eq = index_local_equations status#eq_cache status in
let status = NTactics.merge_tac status in
else
(* we reindex the equation from scratch *)
let unit_eq = index_local_equations status#eq_cache status in
let status = NTactics.merge_tac status in