diff options
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 17 |
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) |