warn "in Ring.elim_type_tac";
Tacticals.thens ~start:(cut_tac ~term)
~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
warn "in Ring.elim_type_tac";
Tacticals.thens ~start:(cut_tac ~term)
~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status