aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml5
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/pfedit.ml25
-rw-r--r--proofs/pfedit.mli43
-rw-r--r--proofs/proof_trees.ml30
-rw-r--r--proofs/refiner.ml99
-rw-r--r--proofs/refiner.mli7
-rw-r--r--proofs/tacinterp.ml17
-rw-r--r--proofs/tacmach.ml27
-rw-r--r--proofs/tacmach.mli14
10 files changed, 118 insertions, 151 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 8276188566..4c2cbf9873 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -33,10 +33,9 @@ type 'a clausenv = {
type wc = walking_constraints
let new_evar_in_sign env =
- let hyps = Environ.var_context env in
+ let ids = ids_of_var_context (Environ.var_context env) in
let ev = new_evar () in
- DOPN(Evar ev,
- Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)))
+ DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) ids))
let rec whd_evar env sigma = function
| DOPN(Evar ev,_) as k ->
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b73d19ee91..abfe2305db 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -100,7 +100,7 @@ let w_add_sign (id,t) (wc : walking_constraints) =
ids_mk (ts_mod
(fun evr ->
{ focus = evr.focus;
- env = push_var (id,t) evr.env;
+ env = push_var_decl (id,t) evr.env;
decls = evr.decls })
(ids_it wc))
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fa69b6e73e..6bea1e8199 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -116,11 +116,11 @@ let get_current_proof_name () =
let add_proof (na,pfs,ts) =
Edit.create proof_edits (na,pfs,ts,Some !undo_limit)
-let del_proof na =
+let delete_proof na =
try
Edit.delete proof_edits na
with (UserError ("Edit.delete",_)) ->
- errorlabstrm "Pfedit.del_proof"
+ errorlabstrm "Pfedit.delete_proof"
[< 'sTR"No such proof" ; msg_proofs false >]
let init_proofs () = Edit.clear proof_edits
@@ -142,7 +142,7 @@ let restart_proof () =
errorlabstrm "Pfedit.restart"
[< 'sTR"No focused proof to restart" ; msg_proofs true >]
| Some(na,_,ts) ->
- del_proof na;
+ delete_proof na;
start (na,ts);
set_current_proof na
@@ -178,16 +178,15 @@ let undo n =
errorlabstrm "Pfedit.undo" [< 'sTR"No focused proof"; msg_proofs true >]
(*********************************************************************)
-(* Proof releasing *)
+(* Proof cooking *)
(*********************************************************************)
-let release_proof () =
+let cook_proof () =
let (pfs,ts) = get_state()
and ident = get_current_proof_name () in
let {evar_concl=concl} = ts.top_goal
and strength = ts.top_strength in
let pfterm = extract_pftreestate pfs in
- del_proof ident;
(ident,
({ const_entry_body = Cooked pfterm; const_entry_type = Some concl },
strength))
@@ -204,11 +203,9 @@ let check_no_pending_proofs () =
[< 'sTR"Proof editing in progress" ; (msg_proofs false) ;
'sTR"Use \"Abort All\" first or complete proof(s)." >]
-let abort_proof = del_proof
+let delete_current_proof () = delete_proof (get_current_proof_name ())
-let abort_current_proof () = del_proof (get_current_proof_name ())
-
-let abort_all_proofs = init_proofs
+let delete_all_proofs = init_proofs
(*********************************************************************)
(* Modifying the current prooftree *)
@@ -238,14 +235,6 @@ let solve_nth k tac =
let pft = get_pftreestate() in
if not (List.mem (-1) (cursor_of_pftreestate pft)) then
mutate (solve_nth_pftreestate k tac)
- (* ;
- let pfs =get_pftreestate() in
- let pf = proof_of_pftreestate pfs in
- let (pfterm,metamap) = refiner__extract_open_proof pf.goal.hyps pf
- in (try typing__control_only_guard empty_evd pfterm
- with e -> (undo 1; raise e));
- ())
- *)
else
error "cannot apply a tactic when we are descended behind a tactic-node"
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 0bf91510b6..a796cd1f44 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -29,19 +29,19 @@ val refining : unit -> bool
val check_no_pending_proofs : unit -> unit
-(*s [abort_proof name] aborts proof of name [name] or failed if no proof
-has this name *)
+(*s [delete_proof name] deletes proof of name [name] or failed if no proof
+ has this name *)
-val abort_proof : identifier -> unit
+val delete_proof : identifier -> unit
-(* [abort_current_proof ()] aborts current focused proof or failed if
+(* [delete_current_proof ()] deletes current focused proof or failed if
no proof is focused *)
-val abort_current_proof : unit -> unit
+val delete_current_proof : unit -> unit
-(* [abort_all_proofs ()] aborts all open proofs if any *)
+(* [delete_all_proofs ()] deletes all open proofs if any *)
-val abort_all_proofs : unit -> unit
+val delete_all_proofs : unit -> unit
(*s [undo n] undoes the effect of the last [n] tactics applied to the
current proof; it fails if no proof is focused or if the ``undo''
@@ -82,13 +82,11 @@ val resume_proof : identifier -> unit
val suspend_proof : unit -> unit
-(*s [release_proof ()] turns the current proof into a constant with
- its name and strength, then remove the proof from the set of
- pending proofs; it fails if there is no current proof of if it is
- not completed *)
+(*s [cook_proof ()] turns the current proof (assumed completed)
+ into a constant with its name and strength; it fails if there is
+ no current proof of if it is not completed *)
-val release_proof : unit ->
- identifier * (Declarations.constant_entry * strength)
+val cook_proof : unit -> identifier * (Declarations.constant_entry * strength)
(*s [get_pftreestate ()] returns the current focused pending proof or
raises [UserError "no focused proof"] *)
@@ -145,22 +143,3 @@ val traverse : int -> unit
val traverse_nth_goal : int -> unit
val traverse_next_unproven : unit -> unit
val traverse_prev_unproven : unit -> unit
-
-(*i N'ont pas à être exportées
-type proof_topstate
-val msg_proofs : bool -> std_ppcmds
-val undo_limit : int ref
-val get_state : unit -> pftreestate * proof_topstate
-val get_topstate : unit -> proof_topstate
-val add_proof : string * pftreestate * proof_topstate -> unit
-val del_proof : string -> unit
-val init_proofs : unit -> unit
-
-val mutate : (pftreestate -> pftreestate) -> unit
-val rev_mutate : (pftreestate -> pftreestate) -> unit
-val start : string * proof_topstate -> unit
-val proof_term : unit -> constr
-val save_anonymous : bool -> string -> unit
-val traverse_to : int list -> unit
-i*)
-
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index e6150fba66..438f0efe3d 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -147,7 +147,7 @@ let ctxt_access sigma sp =
let pf_lookup_name_as_renamed hyps ccl s =
- Detyping.lookup_name_as_renamed (gLOB hyps) ccl s
+ Detyping.lookup_name_as_renamed hyps ccl s
let pf_lookup_index_as_renamed ccl n =
Detyping.lookup_index_as_renamed ccl n
@@ -166,7 +166,7 @@ open Printer
term_env *)
let pf_lookup_name_as_renamed hyps ccl s =
- Detyping.lookup_name_as_renamed (gLOB hyps) ccl s
+ Detyping.lookup_name_as_renamed hyps ccl s
let pf_lookup_index_as_renamed ccl n =
Detyping.lookup_index_as_renamed ccl n
@@ -174,16 +174,15 @@ let pf_lookup_index_as_renamed ccl n =
let pr_idl idl = prlist_with_sep pr_spc print_id idl
let pr_goal g =
- let sign = context g.evar_env in
- let penv = pr_env_opt sign in
- let pc = prterm_env_at_top sign g.evar_concl in
+ let penv = pr_context_of g.evar_env in
+ let pc = prterm_env_at_top g.evar_env g.evar_concl in
[< 'sTR" "; hV 0 [< penv; 'fNL;
'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
'sTR "============================"; 'fNL ;
'sTR" " ; pc>]; 'fNL>]
let pr_concl n g =
- let pc = prterm_env_at_top (context g.evar_env) g.evar_concl in
+ let pc = prterm_env_at_top g.evar_env g.evar_concl in
[< 'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
'sTR "subgoal ";'iNT n;'sTR " is:";'cUT;'sTR" " ; pc >]
@@ -233,16 +232,9 @@ let pr_seq evd =
| Some i -> i
| None -> anomaly "pr_seq : info = None"
in
- let hyps = var_context env in
- let sign = List.rev (list_of_sign hyps) in
let pc = pr_ctxt info in
- let pdcl =
- prlist_with_sep pr_spc
- (fun (id,ty) ->
- hOV 0 [< print_id id; 'sTR" : ";prterm (body_of_type ty) >])
- sign
- in
- let pcl = prterm_env_at_top (gLOB hyps) cl in
+ let pdcl = pr_var_context_of env in
+ let pcl = prterm_env_at_top env cl in
hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
let prgl gl =
@@ -252,13 +244,13 @@ let prgl gl =
let pr_evgl gl =
let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
- let phyps = pr_idl (ids_of_sign (var_context gl.evar_env)) in
+ let phyps = pr_idl (ids_of_var_context (var_context gl.evar_env)) in
let pc = prterm gl.evar_concl in
hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
let pr_evgl_sign gl =
let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
- let ps = pr_sign (var_context gl.evar_env) in
+ let ps = pr_var_context_of gl.evar_env in
let pc = prterm gl.evar_concl in
hOV 0 [< 'sTR"[[" ; plc ; 'sTR"] " ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
@@ -352,7 +344,7 @@ let ast_of_cvt_arg = function
| Integer n -> num n
| Command c -> ope ("COMMAND",[c])
| Constr c ->
- ope ("COMMAND",[ast_of_constr false (assumptions_for_print []) c])
+ ope ("COMMAND",[ast_of_constr false (Global.env ()) c])
| Clause idl -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl)
| Bindings bl -> ope ("BINDINGS",
List.map (ast_of_cvt_bind (fun x -> x)) bl)
@@ -360,7 +352,7 @@ let ast_of_cvt_arg = function
ope ("BINDINGS",
List.map
(ast_of_cvt_bind
- (ast_of_constr false (assumptions_for_print []))) bl)
+ (ast_of_constr false (Global.env ()))) bl)
| Tacexp ast -> ope ("TACTIC",[ast])
| Tac tac -> failwith "TODO: ast_of_cvt_arg: Tac"
| Redexp red -> failwith "TODO: ast_of_cvt_arg: Redexp"
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 1a16f77448..333287b3ed 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -44,7 +44,7 @@ let norm_goal sigma gl =
let red_fun = nf_ise1 sigma in
let ncl = red_fun gl.evar_concl in
{ evar_concl = ncl;
- evar_env = change_hyps (map_sign_typ (typed_app red_fun)) gl.evar_env;
+ evar_env = map_context red_fun gl.evar_env;
evar_body = gl.evar_body;
evar_info = gl.evar_info }
@@ -74,9 +74,10 @@ let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
let m,l = list_chop h l in
(List.hd fl m) :: (mapshape t (List.tl fl) l)
-(* given a proof p, frontier p gives (l,v) where l is the list of goals
+(* frontier : proof_tree -> goal list * validation
+ given a proof p, frontier p gives (l,v) where l is the list of goals
to be solved to complete the proof, and v is the corresponding validation *)
-
+
let rec frontier p =
match p.ref with
| None ->
@@ -230,17 +231,14 @@ let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
(* rc_of_glsigma : proof sigma -> readable_constraints *)
let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
-(* extract_open_proof : constr signature -> proof
- -> constr * (int * constr) list
- takes a constr signature corresponding to global definitions
- and a (not necessarly complete) proof
- and gives a pair (pfterm,obl)
+(* extract_open_proof : proof_tree -> constr * (int * constr) list
+ takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
where pfterm is the constr corresponding to the proof
and obl is an int*constr list [ (m1,c1) ; ... ; (mn,cn)]
where the mi are metavariables numbers, and ci are their types.
Their proof should be completed in order to complete the initial proof *)
-let extract_open_proof sign pf =
+let extract_open_proof sigma pf =
let open_obligations = ref [] in
let rec proof_extractor vl = function
| {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
@@ -255,42 +253,31 @@ let extract_open_proof sign pf =
| {ref=Some(Local_constraints lc,[pf])} -> (proof_extractor vl) pf
| {ref=None;goal=goal} ->
- let n_rels = number_of_rels vl in
let visible_rels =
map_succeed
(fun id ->
- match lookup_id id vl with
- | GLOBNAME _ -> failwith "caught"
- | RELNAME(n,_) -> (n,id))
- (ids_of_sign (evar_hyps goal)) in
- let sorted_rels =
- Sort.list (fun (n1,_) (n2,_) -> n1>n2) visible_rels in
+ try let n = list_index id vl in (n,id)
+ with Not_found -> failwith "caught")
+ (ids_of_var_context (evar_hyps goal)) in
+ let sorted_rels =
+ Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
let abs_concl =
List.fold_right
(fun (_,id) concl ->
- let (_,ty) = lookup_sign id (evar_hyps goal) in
- mkNamedProd id (incast_type ty) concl)
+ let (c,ty) = lookup_id id (evar_hyps goal) in
+ mkNamedProd_or_LetIn (id,c,ty) concl)
sorted_rels goal.evar_concl
in
+ let ass = Retyping.get_assumption_of goal.evar_env sigma abs_concl in
let mv = new_meta() in
- open_obligations := (mv,abs_concl):: !open_obligations;
+ open_obligations := (mv,ass):: !open_obligations;
applist(DOP0(Meta mv),List.map (fun (n,_) -> Rel n) sorted_rels)
| _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
in
- let pfterm = proof_extractor (gLOB sign) pf in
+ let pfterm = proof_extractor [] pf in
(pfterm, List.rev !open_obligations)
-(* extracts a constr from a proof, and raises an error if the proof is
- incomplete *)
-
-let extract_proof sign pf =
- match extract_open_proof sign pf with
- | t,[] -> t
- | _ -> errorlabstrm "extract_proof"
- [< 'sTR "Attempt to save an incomplete proof" >]
-
-
(*********************)
(* Tacticals *)
(*********************)
@@ -554,7 +541,11 @@ let tactic_list_tactic tac gls =
-(* solve_subgoal n tac pf_sigma applies the tactic tac at the nth subgoal of
+(* solve_subgoal :
+ (global_constraints ref * goal list * validation ->
+ global_constraints ref * goal list * validation) ->
+ (proof_tree sigma -> proof_tree sigma)
+ solve_subgoal tac pf_sigma applies the tactic tac at the nth subgoal of
pf_sigma *)
let solve_subgoal tacl pf_sigma =
let (sigr,pf) = unpackage pf_sigma in
@@ -587,7 +578,7 @@ type pftreestate = {
let proof_of_pftreestate pts = pts.tpf
let is_top_pftreestate pts = pts.tstack = []
let cursor_of_pftreestate pts = List.map fst pts.tstack
-let evc_of_pftreestate pts = pts.tpfsigma
+let evc_of_pftreestate pts = ts_it pts.tpfsigma
let top_goal_of_pftreestate pts =
{ it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
@@ -649,12 +640,12 @@ let change_constraints_pftreestate newgc pts =
(* solve the nth subgoal with tactic tac *)
let solve_nth_pftreestate n tac pts =
- let pf = pts.tpf in
- let rslts =
- solve_subgoal (theni_tac n tac) {it = pts.tpf;sigma = pts.tpfsigma} in
- { tpf = rslts.it;
- tpfsigma = rslts.sigma;
- tstack = pts.tstack }
+ let rslts =
+ solve_subgoal (theni_tac n tac) {it = pts.tpf;sigma = pts.tpfsigma}
+ in
+ { tpf = rslts.it;
+ tpfsigma = rslts.sigma;
+ tstack = pts.tstack }
let solve_pftreestate = solve_nth_pftreestate 1
@@ -678,15 +669,19 @@ let mk_pftreestate g =
proof is not complete or the state does not correspond to the head
of the proof-tree *)
+let extract_open_pftreestate pts =
+ extract_open_proof (ts_it pts.tpfsigma) pts.tpf
+
let extract_pftreestate pts =
if pts.tstack <> [] then
errorlabstrm "extract_pftreestate"
[< 'sTR"Cannot extract from a proof-tree in which we have descended;" ;
'sPC; 'sTR"Please ascend to the root" >];
- let env = pts.tpf.goal.evar_env in
- let hyps = Environ.var_context env in
- strong whd_betaiotaevar env (ts_it pts.tpfsigma)
- (extract_proof hyps pts.tpf)
+ let pfterm,subgoals = extract_open_pftreestate pts in
+ if subgoals <> [] then
+ errorlabstrm "extract_proof"
+ [< 'sTR "Attempt to save an incomplete proof" >];
+ strong whd_betaiotaevar pts.tpf.goal.evar_env (ts_it pts.tpfsigma) pfterm
(* Focus on the first leaf proof in a proof-tree state *)
@@ -811,18 +806,22 @@ let pr_rule = function
| Context ctxt -> pr_ctxt ctxt
| Local_constraints lc -> [< 'sTR"Local constraint change" >]
-let thin_sign osign sign =
- sign_it
- (fun id ty nsign ->
- if (not (mem_sign osign id))
- or (id,ty) <> (lookup_sign id osign) (* Hum, egalité sur les types *)
- then add_sign (id,ty) nsign
- else nsign) sign nil_sign
+exception Different
+
+(* We remove from the var context of env what is already in osign *)
+let thin_sign osign env =
+ process_var_context
+ (fun env (id,c,ty as d) ->
+ try
+ if lookup_id id osign = (c,ty) then env
+ else raise Different
+ with Not_found | Different -> push_var d env)
+ env
let rec print_proof sigma osign pf =
let {evar_env=env; evar_concl=cl;
evar_info=info; evar_body=body} = pf.goal in
- let env' = change_hyps (fun sign -> thin_sign osign sign) env in
+ let env' = thin_sign osign env in
match pf.ref with
| None ->
hOV 0 [< pr_seq {evar_env=env'; evar_concl=cl;
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5c2b24d7fc..8546b0c73c 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -39,10 +39,6 @@ val frontier : transformation_tactic
val list_pf : proof_tree -> goal list
val unTAC : tactic -> goal sigma -> proof_tree sigma
-val extract_open_proof :
- typed_type signature -> proof_tree -> constr * (int * constr) list
-
-
(*s Tacticals. *)
(* [tclIDTAC] is the identity tactic *)
@@ -114,7 +110,7 @@ type pftreestate
val proof_of_pftreestate : pftreestate -> proof_tree
val cursor_of_pftreestate : pftreestate -> int list
val is_top_pftreestate : pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> global_constraints
+val evc_of_pftreestate : pftreestate -> evar_declarations
val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
@@ -127,6 +123,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate
val weak_undo_pftreestate : pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
+val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
val extract_pftreestate : pftreestate -> constr
val first_unproven : pftreestate -> pftreestate
val last_unproven : pftreestate -> pftreestate
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c95424fb18..cb8eb0c454 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -45,12 +45,6 @@ let constr_of_Constr = function
| Constr c -> c
| _ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">]
-(* Transforms a type_judgment signature into a (string * constr) list *)
-let make_hyps hyps =
- let lid = List.map string_of_id (ids_of_sign hyps)
- and lhyp = List.map body_of_type (vals_of_sign hyps) in
- List.rev (List.combine lid lhyp)
-
(* Extracted the constr list from lfun *)
let rec constr_list goalopt = function
| (str,VArg(Constr c))::tl -> (id_of_string str,c)::(constr_list goalopt tl)
@@ -62,7 +56,7 @@ let rec constr_list goalopt = function
(match goalopt with
| None -> constr_list goalopt tl
| Some goal ->
- if List.mem_assoc (string_of_id id) (make_hyps (pf_hyps goal)) then
+ if mem_var_context id (pf_hyps goal) then
(id_of_string str,VAR id)::(constr_list goalopt tl)
else
constr_list goalopt tl))
@@ -287,12 +281,11 @@ let apply_matching pat csr =
PatternMatchingFailure -> raise No_match
(* Tries to match one hypothesis with a list of hypothesis patterns *)
-let apply_one_hyp_context lmatch mhyps (idhyp,hyp) =
+let apply_one_hyp_context lmatch mhyps (idhyp,bodyopt,hyp) =
let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc = function
| (Hyp (idpat,pat))::tl ->
(try
- ([idpat,VArg (Identifier
- (id_of_string idhyp))],verify_metas_coherence lmatch
+ ([idpat,VArg (Identifier idhyp)],verify_metas_coherence lmatch
(Pattern.matches pat hyp),mhyps_acc@tl)
with
PatternMatchingFailure | Not_coherent_metas ->
@@ -307,7 +300,7 @@ let apply_one_hyp_context lmatch mhyps (idhyp,hyp) =
apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[NoHypId pat])
tl)
| [] -> raise No_match in
- apply_one_hyp_context_rec (idhyp,hyp) [] mhyps
+ apply_one_hyp_context_rec (idhyp,body_of_type hyp) [] mhyps
(* Prepares the lfun list for constr substitutions *)
let rec make_subs_list = function
@@ -473,7 +466,7 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr =
(try eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal)) t goal
with No_match -> apply_match_context evc env lfun lmatch goal tl)
| (Pat (mhyps,mgoal,mt))::tl ->
- let hyps = make_hyps (pf_hyps goal)
+ let hyps = pf_hyps goal
and concl = pf_concl goal in
(try
(let lgoal = apply_matching mgoal concl in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 9471b5d258..1488b06dee 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -40,19 +40,27 @@ let pf_env gls = (sig_it gls).evar_env
let pf_hyps gls = var_context (sig_it gls).evar_env
let pf_concl gls = (sig_it gls).evar_concl
-
+(*
let pf_untyped_hyps gls =
let sign = Environ.var_context (pf_env gls) in
map_sign_typ (fun x -> body_of_type x) sign
+*)
+let pf_hyps_types gls =
+ let sign = Environ.var_context (pf_env gls) in
+ List.map (fun (id,_,x) -> (id,body_of_type x)) sign
+
+let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
-let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
+let pf_last_hyp gl = List.hd (pf_hyps gl)
-let pf_get_hyp gls id =
+let pf_get_hyp_typ gls id =
try
- snd (lookup_sign id (pf_untyped_hyps gls))
+ body_of_type (snd (lookup_id id (pf_hyps gls)))
with Not_found ->
error ("No such hypothesis : " ^ (string_of_id id))
+let pf_ids_of_hyps gls = ids_of_var_context (var_context (pf_env gls))
+
let pf_ctxt gls = get_ctxt (sig_it gls)
let pf_interp_constr gls c =
@@ -135,6 +143,7 @@ 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
@@ -218,6 +227,12 @@ let unTAC = unTAC
let refiner = refiner
+(* This does not check that the variable name is not here *)
+let unsafe_introduction id =
+ without_check
+ (refiner (Prim { name = Intro; newids = [id];
+ hypspecs = []; terms = []; params = [] }))
+
let introduction id pf =
refiner (Prim { name = Intro; newids = [id];
hypspecs = []; terms = []; params = [] }) pf
@@ -259,7 +274,7 @@ let mutual_cofix lf lar pf =
let rename_bound_var_goal gls =
let { evar_env = env; evar_concl = cl } as gl = sig_it gls in
- let ids = ids_of_sign (Environ.var_context env) in
+ let ids = ids_of_var_context (Environ.var_context env) in
convert_concl (rename_bound_var ids cl) gls
@@ -473,7 +488,7 @@ open Printer
let pr_com sigma goal com =
prterm (rename_bound_var
- (ids_of_sign (var_context goal.evar_env))
+ (ids_of_var_context (var_context goal.evar_env))
(Astterm.interp_constr sigma goal.evar_env com))
let pr_one_binding sigma goal = function
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 60be331742..6ae4f9ae26 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,8 +34,11 @@ val apply_sig_tac :
val pf_concl : goal sigma -> constr
val pf_env : goal sigma -> env
val pf_hyps : goal sigma -> var_context
-val pf_untyped_hyps : goal sigma -> constr signature
-val pf_nth_hyp : goal sigma -> int -> identifier * constr
+(*val pf_untyped_hyps : goal sigma -> (identifier * constr) list*)
+val pf_hyps_types : goal sigma -> (identifier * constr) list
+val pf_nth_hyp_id : goal sigma -> int -> identifier
+val pf_last_hyp : goal sigma -> var_declaration
+val pf_ids_of_hyps : goal sigma -> identifier list
val pf_ctxt : goal sigma -> ctxtty
val pf_global : goal sigma -> identifier -> constr
val pf_parse_const : goal sigma -> string -> constr
@@ -45,9 +48,9 @@ val pf_execute : goal sigma -> constr -> unsafe_judgment
val hnf_type_of : goal sigma -> constr -> constr
val pf_interp_constr : goal sigma -> Coqast.t -> constr
-val pf_interp_type : goal sigma -> Coqast.t -> constr
+val pf_interp_type : goal sigma -> Coqast.t -> constr
-val pf_get_hyp : goal sigma -> identifier -> constr
+val pf_get_hyp_typ : goal sigma -> identifier -> constr
val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
@@ -88,7 +91,7 @@ type pftreestate
val proof_of_pftreestate : pftreestate -> proof_tree
val cursor_of_pftreestate : pftreestate -> int list
val is_top_pftreestate : pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> global_constraints
+val evc_of_pftreestate : pftreestate -> evar_declarations
val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
val traverse : int -> pftreestate -> pftreestate
@@ -96,6 +99,7 @@ val weak_undo_pftreestate : pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
+val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
val extract_pftreestate : pftreestate -> constr
val first_unproven : pftreestate -> pftreestate
val last_unproven : pftreestate -> pftreestate
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:11:12 +0000