diff options
Diffstat (limited to 'proofs/proof_trees.ml')
-rw-r--r-- | proofs/proof_trees.ml | 27 |
1 files changed, 22 insertions, 5 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 7e299b89..9d70d012 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 6113 2004-09-17 20:28:19Z barras $ *) +(* $Id: proof_trees.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Closure open Util @@ -18,6 +18,7 @@ open Sign open Evd open Environ open Evarutil +open Decl_expr open Proof_type open Tacred open Typing @@ -32,9 +33,9 @@ let is_bind = function (* Functions on goals *) -let mk_goal hyps cl = +let mk_goal hyps cl extra = { evar_hyps = hyps; evar_concl = cl; - evar_body = Evar_empty} + evar_body = Evar_empty; evar_extra = extra } (* Functions on proof trees *) @@ -52,7 +53,7 @@ let children_of_proof pf = let goal_of_proof pf = pf.goal let subproof_of_proof pf = match pf.ref with - | Some (Tactic (_,pf), _) -> pf + | Some (Nested (_,pf), _) -> pf | _ -> failwith "subproof_of_proof" let status_of_proof pf = pf.open_subgoals @@ -62,7 +63,7 @@ let is_complete_proof pf = pf.open_subgoals = 0 let is_leaf_proof pf = (pf.ref = None) let is_tactic_proof pf = match pf.ref with - | Some (Tactic _, _) -> true + | Some (Nested (Tactic _,_),_) -> true | _ -> false @@ -72,6 +73,22 @@ let pf_lookup_name_as_renamed 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) *) + +let is_dem_rule = function + Decl_proof _ -> true + | _ -> false + +let is_proof_instr = function + Nested(Proof_instr (_,_),_) -> true + | _ -> false + +let is_focussing_command = function + Decl_proof b -> b + | Nested (Proof_instr (b,_),_) -> b + | _ -> false + + (*********************************************************************) (* Pretty printing functions *) (*********************************************************************) |