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                        *)
 (*********************************************************************)