diff options
| author | corbinea | 2006-09-20 17:18:18 +0000 |
|---|---|---|
| committer | corbinea | 2006-09-20 17:18:18 +0000 |
| commit | 0f4f723a5608075ff4aa48290314df30843efbcb (patch) | |
| tree | 09316ca71749b9218972ca801356388c04d29b4c /proofs/proof_type.mli | |
| parent | c6b9d70f9292fc9f4b5f272b5b955af0e8fe0bea (diff) | |
Declarative Proof Language: main commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index e222730582..74c36c9811 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -16,6 +16,7 @@ open Libnames open Term open Util open Tacexpr +open Decl_expr open Rawterm open Genarg open Nametab @@ -46,7 +47,7 @@ type prim_rule = evar_body = Evar_Empty; evar_info = { pgm : [The Realizer pgm if any] lc : [Set of evar num occurring in subgoal] }} - sigma = { stamp = [an int characterizing the ed field, for quick compare] + sigma = { stamp = [an int chardacterizing the ed field, for quick compare] ed : [A set of existential variables depending in the subgoal] number of first evar, it = { evar_concl = [the type of first evar] @@ -80,9 +81,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 + and goal = evar_info and tactic = goal sigma -> (goal list sigma * validation) |