X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fring.ml;h=66541d1b0e18acb9f2855e649b9bac6f926b659e;hb=4cbd4cadc2e71d4d25469dd7dddf05088baacb62;hp=399d2c2892334297ed970f25b47fe363ede544e8;hpb=373eaf73bebec626e031a4a534ddfdd4f1c1b474;p=helm.git

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 399d2c289..66541d1b0 100644
--- a/helm/gTopLevel/ring.ml
+++ b/helm/gTopLevel/ring.ml
@@ -404,6 +404,7 @@ let status_of_single_goal_tactic_result =
   | _ ->
     raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
 
+(* Galla: spostata in variousTactics.ml 
   (**
     auxiliary tactic "elim_type"
     @param status current proof engine status
@@ -413,6 +414,7 @@ let elim_type_tac ~term ~status =
   warn "in Ring.elim_type_tac";
   Tacticals.thens ~start:(cut_tac ~term)
    ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
+*)
 
   (**
     auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
@@ -422,10 +424,10 @@ let elim_type_tac ~term ~status =
   *)
 let elim_type2_tac ~term ~proof ~status =
   warn "in Ring.elim_type2";
-  Tacticals.thens ~start:(elim_type_tac ~term)
+  Tacticals.thens ~start:(VariousTactics.elim_type_tac ~term)
    ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
 
-(* spostata in variousTactics.ml
+(* Galla: spostata in variousTactics.ml
   (**
     Reflexivity tactic, try to solve current goal using "refl_eqT"
     Warning: this isn't equale to the coq's Reflexivity because this one tries