Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry...

[helm.git] / helm / gTopLevel / ring.ml

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index d30df1aaa23629169118a6cb95211a0207c4aae4..399d2c2892334297ed970f25b47fe363ede544e8 100644 (file)
--- a/helm/gTopLevel/ring.ml
+++ b/helm/gTopLevel/ring.ml
@@ -397,8 +397,6 @@ let build_segments ~terms =
      Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t]
    ) aterms
 
-let id_tac ~status:(proof,goal) =
- (proof,[goal])
 
 let status_of_single_goal_tactic_result =
  function
@@ -414,7 +412,7 @@ let status_of_single_goal_tactic_result =
 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) ; id_tac] ~status
+   ~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
@@ -425,8 +423,9 @@ 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)
-   ~continuations:[id_tac ; exact_tac ~term:proof] ~status
+   ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
 
+(* 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
@@ -441,6 +440,7 @@ let reflexivity_tac ~status:(proof, goal) =
   with (Fail _) as e ->
     let e_str = Printexc.to_string e in
     raise (Fail ("Reflexivity failed with exception: " ^ e_str))
+*)
 
   (** lift an 8-uple of debrujins indexes of n *)
 let lift ~n (a,b,c,d,e,f,g,h) =
@@ -498,7 +498,7 @@ let ring_tac ~status:((proof, goal) as status) =
         Tacticals.try_tactics
           ~status
           ~tactics:[
-            "reflexivity", reflexivity_tac ;
+            "reflexivity", VariousTactics.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
@@ -570,7 +570,7 @@ let ring_tac ~status:((proof, goal) as status) =
                       in
                       try (* try to solve main goal *)
                         warn "trying reflexivity ....";
-                        reflexivity_tac ~status:status'
+                        VariousTactics.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')]