diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-23 18:18:13 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-23 18:18:13 +0000 |
| commit | b946944cb9bb21dcd9aba3b01b9aeafc4b78b1c8 (patch) | |
| tree | f76ac391e9b302c716b862163eeaccd2ad5d899f /CHANGES | |
| parent | ea798f046bf172626bd229906946803b0dd9cd96 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -165,7 +165,7 @@ Tactic language - Fail tactic now accepts a failure message - Idtac tactic now accepts a message -- New primitive tactic "FreshId" (new syntax: "Fresh") to generate new names +- New primitive tactic "FreshId" (new syntax: "fresh") to generate new names - Debugger prints levels of calls Tactics @@ -195,6 +195,8 @@ Tactics immediate hint), resulting in shorter proofs - Instantiate now works in hyps (syntax : Instantiate in ...) - Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists +- Clear now fails when trying to remove a local definition used by + a constant appearing in the current goal Extraction (See details in contrib/extraction/CHANGES) |