let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) =
- VariousTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
+ EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
~status:((curi,metasenv',pbo,pty),goal)
in
let new_goals = fresh_meta::goals in
|_-> (proof,[goal])
;;
-
+(* Galla: moved in variousTactics.ml
let assumption_tac ~status:(proof,goal)=
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
in
Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
;;
-
+*)
+(* Galla: moved in negationTactics.ml
(* !!!!! fix !!!!!!!!!! *)
let contradiction_tac ~status:(proof,goal)=
Tacticals.then_
(*inutile sia questo che quello prima della chiamata*)
- ~start:
- (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
+ ~start:PrimitiveTactics.intros_tac
~continuation:(Tacticals.then_
~start:(VariousTactics.elim_type_tac ~term:_False)
~continuation:(assumption_tac))
~status:(proof,goal)
;;
+*)
(* ********************* TATTICA ******************************** *)
(* now let's change our thesis applying the th and put it with hp *)
- let proof,gl = Tacticals.then_
- ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
- ~continuation:
- (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
- ~status:(s_proof,s_goal) in
+ let proof,gl =
+ Tacticals.then_
+ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+ ~continuation:PrimitiveTactics.intros_tac
+ ~status:(s_proof,s_goal) in
let goal = if List.length gl = 1 then List.hd gl
else failwith "a new goal" in