X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;h=c505807f2ddc24295a060912d90fd3602cb7bfb3;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=298a87f3c8df8361fc4bcaee9f9cbaa5dc12c5d9;hpb=c792b3d48316f63cd1066b5901cf859496d71052;p=helm.git

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 298a87f3c..c505807f2 100644
--- 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 ...",