let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
in
let fail_tac =
let fail_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _ , _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
back to obtain the result of the tactic *)
let mk_tactic f =
PET.mk_tactic
- (fun (proof, goal) as pstatus ->
+ (fun ((proof, goal) as pstatus) ->
let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
let istatus = pstatus, stack in
let (proof, _, _), stack = f istatus in
(* Tacticals that cannot be implemented on top of tynycals *)
let first ~tactics =
- let rec first ~(tactics: (string * tactic) list) status =
+ let rec first ~(tactics: tactic list) status =
info (lazy "in Tacticals.first");
match tactics with
[] -> raise (PET.Fail (lazy "first: no tactics left"))
- | (descr, tac)::tactics ->
- info (lazy ("Tacticals.first IS TRYING " ^ descr));
+ | tac::tactics ->
try
let res = PET.apply_tactic tac status in
- info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
+ info (lazy ("Tacticals.first: succedeed!!!"));
res
with
PET.Fail _ -> first ~tactics status
(* This tries tactics until one of them solves the goal *)
let solve_tactics ~tactics =
- let rec solve_tactics ~(tactics: (string * tactic) list) status =
+ let rec solve_tactics ~(tactics: tactic list) status =
info (lazy "in Tacticals.solve_tactics");
match tactics with
- | (descr, currenttactic)::moretactics ->
- info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
+ | currenttactic::moretactics ->
(try
let (proof, opened) as output_status =
PET.apply_tactic currenttactic status
in
match opened with
- | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
- " solved the goal!!!"));
+ | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
output_status
| _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
raise (PET.Fail (lazy "Goal not solved"))
let progress_tactic ~tactic =
let msg = lazy "Failed to progress" in
- let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
- let ((_,metasenv',_,_,_),_) as ostatus =
+ let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
+ let ((_,metasenv',_subst,_,_,_),_) as ostatus =
PET.apply_tactic tactic istatus
in
(*CSC: Warning