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
| _ ->
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
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
*)
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
+ Tacticals.thens ~start:(VariousTactics.elim_type_tac ~term)
+ ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
+(* 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
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) =
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
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')]