diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-16 09:55:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-16 09:55:24 +0000 |
| commit | 44510966ab7240c60f28f4f2e99d382e155b084b (patch) | |
| tree | ff0ced4a78b1368b41c9f0bbc5145fc5152f4ec6 /proofs | |
| parent | ae06af990c17e462ecc39ef048d664a34e3e2d7d (diff) | |
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
- TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b8de1e789..c2b226281 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -84,6 +84,8 @@ type 'id gclause = onconcl : bool; concl_occs :int list } +let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} + let simple_clause_of = function { onhyps = Some[scl]; onconcl = false } -> Some scl | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None @@ -123,8 +125,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacCofix of identifier option | TacMutualCofix of identifier * (identifier * 'constr) list | TacCut of 'constr - | TacTrueCut of name * 'constr - | TacForward of bool * name * 'constr + | TacAssert of 'tac option * intro_pattern_expr option * 'constr | TacGeneralize of 'constr list | TacGeneralizeDep of 'constr | TacLetTac of name * 'constr * 'id gclause |