diff options
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 4652bac2e..d806d80b8 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -40,14 +40,7 @@ type prim_rule = | Rename of identifier * identifier | Change_evars -type proof_tree = { - goal : goal; - ref : (rule * proof_tree list) option } - -and rule = - | Prim of prim_rule - | Decl_proof of bool - | Daimon +type rule = Prim of prim_rule type compound_rule= | Tactic of tactic_expr * bool |