diff options
| author | herbelin | 2008-10-27 11:38:47 +0000 |
|---|---|---|
| committer | herbelin | 2008-10-27 11:38:47 +0000 |
| commit | e60054fe4dbdc26ed545c7ca6fb8ab36b244f2f7 (patch) | |
| tree | 9afe210d0103863b920989845bd27b0049a97423 /CHANGES | |
| parent | 1c450e282d8e6ae37f687c545776939f2d975cf3 (diff) | |
- Fixed many "Theorem with" bugs.
- Fixed doc of assert as.
- Doc of apply in + update credits.
- Nettoyage partiel de Even.v en utilisant "Theorem with".
- Added check that name is not in use for "generalize as".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -243,6 +243,7 @@ Tactics to remember the term to which the induction or case analysis applied (possible source of parsing incompatibilities when destruct or induction is part of a let-in expression in Ltac; extra parentheses are then required). +- New support for "as" clause in tactics "apply in" and "eapply in". - Some new intro patterns: * intro pattern "?A" genererates a fresh name based on A. Caveat about a slight loss of compatibility: @@ -285,7 +286,7 @@ Tactics - Tactic firstorder "with" and "using" options have their meaning swapped for consistency with auto/eauto (source of incompatibility). - Tactic "generalize" now supports "at" options to specify occurrences - and "as" options to name the hypothesis. + and "as" options to name the quantified hypotheses. - New tactic "specialize H with a" or "specialize (H a)" allows to transform in-place a universally-quantified hypothesis (H : forall x, T x) into its instantiated form (H : T a). Nota: "specialize" was in fact there in earlier |