Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 9 insertions, 8 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 009e9d5b..abe31624 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(*i $Id: proof_type.ml 9244 2006-10-16 17:11:44Z barras $ *)
 
 (*i*)
 open Environ
@@ -16,6 +16,7 @@ open Libnames
 open Term
 open Util
 open Tacexpr
+open Decl_expr
 open Rawterm
 open Genarg
 open Nametab
@@ -39,12 +40,6 @@ type prim_rule =
   | Move of bool * identifier * identifier
   | Rename of identifier * identifier
 
-(*s Proof trees. 
-  [ref] = [None] if the goal has still to be proved, 
-  and [Some (r,l)] if the rule [r] was applied to the goal
-  and gave [l] as subproofs to be completed. 
-  if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
-  that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
   open_subgoals : int;
   goal : goal;
@@ -52,9 +47,15 @@ type proof_tree = {
 
 and rule =
   | Prim of prim_rule
-  | Tactic of tactic_expr * proof_tree
+  | Nested of compound_rule * proof_tree 
+  | Decl_proof of bool
+  | Daimon
   | Change_evars
 
+and compound_rule=  
+  | Tactic of tactic_expr * bool
+  | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
+
 and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)