From 0f4f723a5608075ff4aa48290314df30843efbcb Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 20 Sep 2006 17:18:18 +0000
Subject: Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_type.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'proofs/proof_type.ml')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index db3c0e7e25..4037237026 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -16,6 +16,7 @@ open Libnames
 open Term
 open Util
 open Tacexpr
+open Decl_expr
 open Rawterm
 open Genarg
 open Nametab
@@ -52,9 +53,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
+  | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
+
 and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
-- 
cgit v1.2.3