@param term term to cut
@param proof term used to prove second subgoal generated by elim_type
*)
+(* FG: METTERE I NOMI ANCHE QUI? *)
let elim_type2_tac ~term ~proof =
let elim_type2_tac ~term ~proof status =
let module E = EliminationTactics in
warn "in Ring.elim_type2";
ProofEngineTypes.apply_tactic
- (Tacticals.thens ~start:(E.elim_type_tac ~term)
+ (Tacticals.thens ~start:(E.elim_type_tac term)
~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
in
ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
ProofEngineTypes.apply_tactic
- (Tacticals.try_tactics
+ (Tacticals.first
~tactics:[
"reflexivity", EqualityTactics.reflexivity_tac ;
"exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
in
let status'' =
ProofEngineTypes.apply_tactic
- (Tacticals.try_tactics (* try to solve 1st subgoal *)
+ (Tacticals.first (* try to solve 1st subgoal *)
~tactics:[
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
"exact sym_eqt su t2 ...",