- id_tac ~status
-;;
-
-
-
-
-
-
-
-
-
-
- (** tattica di prova per debuggare i tatticali *)
-(*
-let thens' ~start ~continuations ~status =
- let (proof,new_goals) = start ~status in
- try
- List.fold_left2
- (fun (proof,goals) goal tactic ->
- let (proof',new_goals') = tactic ~status:(proof,goal) in
- (proof',goals@new_goals')
- ) (proof,[]) new_goals continuations
- with
- Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
-
-let prova_tac =
- let apply_T_tac ~status:((proof,goal) as status) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,gty = CicUtil.lookup_meta goal metasenv in
- let rel =
- let rec find n =
- function
- [] -> assert false
- | (Some (Cic.Name name,_))::_ when name = "T" -> n
- | _::tl -> find (n+1) tl
- in
- prerr_endline ("eseguo find");
- find 1 context
- in
- prerr_endline ("eseguo apply");
- apply_tac ~term:(Cic.Rel rel) ~status