X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fring.ml;h=25fa093f20601591b6041fa8eb79808800ebad5f;hb=331dc1783c8572be9d5c7c0ba11fa2995539bbf6;hp=66541d1b0e18acb9f2855e649b9bac6f926b659e;hpb=17d5498ae78a00bc81aaa8d87a925a2d6a2cf050;p=helm.git

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 66541d1b0..25fa093f2 100644
--- a/helm/gTopLevel/ring.ml
+++ b/helm/gTopLevel/ring.ml
@@ -423,8 +423,9 @@ let elim_type_tac ~term ~status =
     @param proof term used to prove second subgoal generated by elim_type
   *)
 let elim_type2_tac ~term ~proof ~status =
+  let module E = EliminationTactics in
   warn "in Ring.elim_type2";
-  Tacticals.thens ~start:(VariousTactics.elim_type_tac ~term)
+  Tacticals.thens ~start:(E.elim_type_tac ~term)
    ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
 
 (* Galla: spostata in variousTactics.ml
@@ -500,7 +501,7 @@ let ring_tac ~status:((proof, goal) as status) =
         Tacticals.try_tactics
           ~status
           ~tactics:[
-            "reflexivity", VariousTactics.reflexivity_tac ;
+            "reflexivity", EqualityTactics.reflexivity_tac ;
             "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
             "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
             "exact sym_eqt su t1 ...", exact_tac
@@ -572,7 +573,7 @@ let ring_tac ~status:((proof, goal) as status) =
                       in
                       try (* try to solve main goal *)
                         warn "trying reflexivity ....";
-                        VariousTactics.reflexivity_tac ~status:status'
+                        EqualityTactics.reflexivity_tac ~status:status'
                       with (Fail _) ->  (* leave conclusion to the user *)
                         warn "reflexivity failed, solution's left as an ex :-)";
                         purge_hyps_tac ~count:!new_hyps ~status:status')]