@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
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
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')]