diff options
| author | corbinea | 2007-01-28 23:30:12 +0000 |
|---|---|---|
| committer | corbinea | 2007-01-28 23:30:12 +0000 |
| commit | 8878a1974cf41ea40e411785d1197f2722a50445 (patch) | |
| tree | d0b61b5adf8290304ee8d90ea4b655550592bbf3 /proofs | |
| parent | 4d5984258731e82c17535cbe9c257cf639374151 (diff) | |
"suffices" implemented + syntax cleanup
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/decl_expr.mli | 9 | ||||
| -rw-r--r-- | proofs/decl_mode.ml | 4 |
2 files changed, 7 insertions, 6 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli index 67a1ea5a64..1c5cc0e746 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.mli @@ -38,7 +38,7 @@ type block_type = | B_elim of elim_type type ('it,'constr,'tac) cut = - {cut_stat: 'it statement; + {cut_stat: 'it; cut_by: 'constr list option; cut_using: 'tac option} @@ -48,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 diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index 2e54f37438..5428166a99 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -68,9 +68,9 @@ type stack_info = type pm_info = { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr ; (* partial goal construction *) + pm_partial_goal : constr; (* partial goal construction *) pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list } + pm_stack : stack_info list} let pm_in,pm_out = Dyn.create "pm_info" |