- ElimIntrosSimpl now implemented using tacticals. It becomes an

[helm.git] / helm / gTopLevel / ring.ml

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 1d614b6f6ac06448884b79bb7a5f8bc157842917..d30df1aaa23629169118a6cb95211a0207c4aae4 100644 (file)
--- a/helm/gTopLevel/ring.ml
+++ b/helm/gTopLevel/ring.ml
@@ -414,7 +414,7 @@ let status_of_single_goal_tactic_result =
 let elim_type_tac ~term ~status =
   warn "in Ring.elim_type_tac";
   Tacticals.thens ~start:(cut_tac ~term)
-   ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status
+   ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; id_tac] ~status
 
   (**
     auxiliary tactic, use elim_type and try to close 2nd subgoal using proof