diff options
Diffstat (limited to 'proofs/decl_expr.mli')
| -rw-r--r-- | proofs/decl_expr.mli | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli index 24af3842..a8b7c0d6 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.mli @@ -6,16 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Names open Util open Tacexpr -type ('constr,'tac) justification = - By_tactic of 'tac -| Automated of 'constr list - type 'it statement = {st_label:name; st_it:'it} @@ -42,8 +38,9 @@ type block_type = | B_elim of elim_type type ('it,'constr,'tac) cut = - {cut_stat: 'it statement; - cut_by: ('constr,'tac) justification} + {cut_stat: 'it; + cut_by: 'constr list option; + cut_using: 'tac option} type ('var,'constr) hyp = Hvar of 'var @@ -51,14 +48,15 @@ type ('var,'constr) hyp = type ('constr,'tac) casee = Real of 'constr - | Virtual of ('constr,'constr,'tac) cut + | Virtual of ('constr statement,'constr,'tac) cut type ('hyp,'constr,'pat,'tac) bare_proof_instr = | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Pcut of ('constr or_thesis,'constr,'tac) cut - | Prew of side * ('constr,'constr,'tac) cut + | Pcut of ('constr or_thesis statement,'constr,'tac) cut + | Prew of side * ('constr statement,'constr,'tac) cut + | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut | Passume of ('hyp,'constr) hyp list | Plet of ('hyp,'constr) hyp list | Pgiven of ('hyp,'constr) hyp list |