X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;fp=helm%2Focaml%2Ftactics%2Fring.ml;h=c505807f2ddc24295a060912d90fd3602cb7bfb3;hb=fddf15f1e9d253316bdcb854c2ff7ec64144bde8;hp=1d5fd903dead5cc09649faf676e9bb310e080b88;hpb=e224f7d4711b700b9e7583ba7452bc7587d1787c;p=helm.git

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 1d5fd903d..c505807f2 100644
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -483,7 +483,7 @@ let ring_tac status =
       try
         let new_hyps = ref 0 in  (* number of new hypotheses created *)
 	ProofEngineTypes.apply_tactic 
-         (Tacticals.try_tactics
+         (Tacticals.first
           ~tactics:[
             "reflexivity", EqualityTactics.reflexivity_tac ;
             "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
@@ -526,7 +526,7 @@ let ring_tac status =
               in
               let status'' =
 	       ProofEngineTypes.apply_tactic
-                (Tacticals.try_tactics (* try to solve 1st subgoal *)
+                (Tacticals.first (* try to solve 1st subgoal *)
                   ~tactics:[
                     "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
                     "exact sym_eqt su t2 ...",