diff options
author | 2010-07-21 09:46:51 +0200 | |
---|---|---|
committer | 2010-07-21 09:46:51 +0200 | |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /proofs/proof_trees.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'proofs/proof_trees.ml')
-rw-r--r-- | proofs/proof_trees.ml | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 99a1e506..a5bd073a 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: proof_trees.ml 10124 2007-09-17 18:40:21Z herbelin $ *) +(* $Id$ *) open Closure open Util @@ -33,10 +33,11 @@ let is_bind = function (* Functions on goals *) -let mk_goal hyps cl extra = - { evar_hyps = hyps; evar_concl = cl; +let mk_goal hyps cl extra = + { evar_hyps = hyps; evar_concl = cl; evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); - evar_body = Evar_empty; evar_extra = extra } + evar_body = Evar_empty; evar_source = (dummy_loc,GoalEvar); + evar_extra = extra } (* Functions on proof trees *) @@ -48,9 +49,9 @@ let ref_of_proof pf = let rule_of_proof pf = let (r,_) = ref_of_proof pf in r -let children_of_proof pf = +let children_of_proof pf = let (_,cl) = ref_of_proof pf in cl - + let goal_of_proof pf = pf.goal let subproof_of_proof pf = match pf.ref with @@ -68,13 +69,13 @@ let is_tactic_proof pf = match pf.ref with | _ -> false -let pf_lookup_name_as_renamed env ccl s = - Detyping.lookup_name_as_renamed env ccl s +let pf_lookup_name_as_displayed env ccl s = + Detyping.lookup_name_as_displayed env ccl s let pf_lookup_index_as_renamed env ccl n = Detyping.lookup_index_as_renamed env ccl n -(* Functions on rules (Proof mode) *) +(* Functions on rules (Proof mode) *) let is_dem_rule = function Decl_proof _ -> true @@ -85,9 +86,9 @@ let is_proof_instr = function | _ -> false let is_focussing_command = function - Decl_proof b -> b - | Nested (Proof_instr (b,_),_) -> b - | _ -> false + Decl_proof b -> b + | Nested (Proof_instr (b,_),_) -> b + | _ -> false (*********************************************************************) |