summaryrefslogtreecommitdiff
path: root/proofs/tacmach.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacmach.ml')
-rw-r--r--proofs/tacmach.ml69
1 files changed, 15 insertions, 54 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 3939a78b..b2a853d7 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacmach.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
@@ -21,7 +19,6 @@ open Evd
open Typing
open Redexpr
open Tacred
-open Proof_trees
open Proof_type
open Logic
open Refiner
@@ -34,7 +31,6 @@ let re_sig it gc = { it = it; sigma = gc }
(**************************************************************)
type 'a sigma = 'a Evd.sigma;;
-type validation = Proof_type.validation;;
type tactic = Proof_type.tactic;;
let unpackage = Refiner.unpackage
@@ -46,7 +42,7 @@ let project = Refiner.project
let pf_env = Refiner.pf_env
let pf_hyps = Refiner.pf_hyps
-let pf_concl gls = (sig_it gls).evar_concl
+let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
let pf_hyps_types gls =
let sign = Environ.named_context (pf_env gls) in
List.map (fun (id,_,x) -> (id, x)) sign
@@ -76,14 +72,6 @@ let pf_get_new_ids ids gls =
(fun id acc -> (next_ident_away id (acc@avoid))::acc)
ids []
-let pf_interp_constr gls c =
- let evc = project gls in
- Constrintern.interp_constr evc (pf_env gls) c
-
-let pf_interp_type gls c =
- let evc = project gls in
- Constrintern.interp_type evc (pf_env gls) c
-
let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
let pf_parse_const gls = compose (pf_global gls) id_of_string
@@ -123,11 +111,11 @@ let pf_matches = pf_apply Matching.matches_conv
(* Tactics handling a list of goals *)
(************************************)
-type transformation_tactic = proof_tree -> (goal list * validation)
+type transformation_tactic = proof_tree -> goal list
type validation_list = proof_tree list -> proof_tree list
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = Refiner.tactic_list
let first_goal = first_goal
let goal_goal_list = goal_goal_list
@@ -138,37 +126,6 @@ let tclFIRSTLIST = tclFIRSTLIST
let tclIDTAC_list = tclIDTAC_list
-(********************************************************)
-(* Functions for handling the state of the proof editor *)
-(********************************************************)
-
-type pftreestate = Refiner.pftreestate
-
-let proof_of_pftreestate = proof_of_pftreestate
-let cursor_of_pftreestate = cursor_of_pftreestate
-let is_top_pftreestate = is_top_pftreestate
-let evc_of_pftreestate = evc_of_pftreestate
-let top_goal_of_pftreestate = top_goal_of_pftreestate
-let nth_goal_of_pftreestate = nth_goal_of_pftreestate
-let traverse = traverse
-let solve_nth_pftreestate = solve_nth_pftreestate
-let solve_pftreestate = solve_pftreestate
-let weak_undo_pftreestate = weak_undo_pftreestate
-let mk_pftreestate = mk_pftreestate
-let extract_pftreestate = extract_pftreestate
-let extract_open_pftreestate = extract_open_pftreestate
-let first_unproven = first_unproven
-let last_unproven = last_unproven
-let nth_unproven = nth_unproven
-let node_prev_unproven = node_prev_unproven
-let node_next_unproven = node_next_unproven
-let next_unproven = next_unproven
-let prev_unproven = prev_unproven
-let top_of_tree = top_of_tree
-let frontier = frontier
-let change_constraints_pftreestate = change_constraints_pftreestate
-
-
(********************************************)
(* Definition of the most primitive tactics *)
(********************************************)
@@ -237,16 +194,20 @@ let rename_hyp l = with_check (rename_hyp_no_check l)
open Pp
open Tacexpr
-open Rawterm
+open Glob_term
-let rec pr_list f = function
- | [] -> mt ()
- | a::l1 -> (f a) ++ pr_list f l1
+let db_pr_goal sigma g =
+ let env = Goal.V82.env sigma g in
+ let penv = print_named_context env in
+ let pc = print_constr_env env (Goal.V82.concl sigma g) in
+ str" " ++ hv 0 (penv ++ fnl () ++
+ str "============================" ++ fnl () ++
+ str" " ++ pc) ++ fnl ()
let pr_gls gls =
- hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
+ hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
let pr_glls glls =
- hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
- prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
+ hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
+ prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls))