X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fring.ml;h=b2d3032706960ca8757588c695cdd16741f48ed2;hb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;hp=0bc26514d45819ce8e4e2e026edf50c7f765519f;hpb=324d594e5e37081d945d631986447a95a1937634;p=helm.git

diff --git a/components/tactics/ring.ml b/components/tactics/ring.ml
index 0bc26514d..b2d303270 100644
--- a/components/tactics/ring.ml
+++ b/components/tactics/ring.ml
@@ -486,10 +486,10 @@ let ring_tac status =
 	ProofEngineTypes.apply_tactic 
          (Tacticals.first
           ~tactics:[
-            "reflexivity", EqualityTactics.reflexivity_tac ;
-            "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
-            "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
-            "exact sym_eqt su t1 ...", exact_tac
+            EqualityTactics.reflexivity_tac ;
+            exact_tac ~term:t1'_eq_t1'' ;
+            exact_tac ~term:t2'_eq_t2'' ;
+            exact_tac
             ~term:(
               Cic.Appl
                [mkConst HelmLibraryObjects.Logic.sym_eq_URI
@@ -499,7 +499,7 @@ let ring_tac status =
                  ] ;
                 t1'_eq_t1''
                ]) ;
-            "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
+            ProofEngineTypes.mk_tactic (fun status ->
               let status' = (* status after 1st elim_type use *)
                 let context = context_of_status status in
 		let b,_ = (*TASSI : FIXME*)
@@ -529,9 +529,8 @@ let ring_tac status =
 	       ProofEngineTypes.apply_tactic
                 (Tacticals.first (* try to solve 1st subgoal *)
                   ~tactics:[
-                    "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
-                    "exact sym_eqt su t2 ...",
-                      exact_tac
+                    exact_tac ~term:t2'_eq_t2'';
+                    exact_tac
                        ~term:(
                          Cic.Appl
                           [mkConst HelmLibraryObjects.Logic.sym_eq_URI
@@ -541,7 +540,6 @@ let ring_tac status =
                             ] ;
                            t2'_eq_t2''
                           ]) ;
-                    "elim_type eqt su t2 ...", 
 		     ProofEngineTypes.mk_tactic (fun status ->
                       let status' =
                         let context = context_of_status status in