| _ ->
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
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
*)
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