1. tactical "try_tacticals" renamed to "first"

[helm.git] / helm / ocaml / tactics / ring.ml

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 1d5fd903dead5cc09649faf676e9bb310e080b88..c505807f2ddc24295a060912d90fd3602cb7bfb3 100644 (file)
--- 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 ...",