- mk_tactic (solve_tactics ~tactics)
-;;
-
-
-
-
-
-
-
-
-
-
- (** 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 (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 =
- let (proof, goal) = status in
- 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
- debug_print ("eseguo find");
- find 1 context
- in
- debug_print ("eseguo apply");
- apply_tac ~term:(Cic.Rel rel) status
- in
-(* do_tactic ~n:2 *)
- repeat_tactic
- ~tactic:
- (then_
- ~start:(intros_tac ~name:"pippo")
- ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)]))
-(* id_tac *)
-;;
-*)
-
-
+ S.mk_tactic (solve_tactics ~tactics)
+end
+
+module ProofEngineStatus =
+ struct
+ type input_status = ProofEngineTypes.status
+ type output_status = ProofEngineTypes.proof * ProofEngineTypes.goal list
+ type tactic = ProofEngineTypes.tactic
+ let id_tac = id_tac
+ let mk_tactic = ProofEngineTypes.mk_tactic
+ let apply_tactic = ProofEngineTypes.apply_tactic
+ let goals (_,goals) = goals
+ let set_goals (proof,_) goals = proof,goals
+ let focus (proof,_) goal = proof,goal
+ end
+
+module ProofEngineTacticals = Make(ProofEngineStatus)
+
+include ProofEngineTacticals