X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fring.ml;h=d30df1aaa23629169118a6cb95211a0207c4aae4;hb=3066e4dcb7270a5eb20020a91d45da9eb87e2f2e;hp=1d614b6f6ac06448884b79bb7a5f8bc157842917;hpb=7074f0403d1bec7f4d60715e50a0fe0ef0993567;p=helm.git

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 1d614b6f6..d30df1aaa 100644
--- 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