version 0.7.1

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

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 298a87f3c8df8361fc4bcaee9f9cbaa5dc12c5d9..c505807f2ddc24295a060912d90fd3602cb7bfb3 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -388,12 +388,13 @@ let elim_type_tac ~term status =
     @param term term to cut
     @param proof term used to prove second subgoal generated by elim_type
   *)
+(* FG: METTERE I NOMI ANCHE QUI? *)  
 let elim_type2_tac ~term ~proof =
  let elim_type2_tac ~term ~proof status =
   let module E = EliminationTactics in
   warn "in Ring.elim_type2";
   ProofEngineTypes.apply_tactic 
-   (Tacticals.thens ~start:(E.elim_type_tac ~term)
+   (Tacticals.thens ~start:(E.elim_type_tac term)
     ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
  in
   ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
@@ -482,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'' ;
@@ -525,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 ...",