diff options
| author | Hugo Herbelin | 2015-12-05 00:42:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 00:58:19 +0100 |
| commit | cbceffe424a6b4477eb822f3887776b587503cbd (patch) | |
| tree | 03b784f5426564c7d74c54d4c7b83a3d6988b2ad | |
| parent | 9ee4a02e9234ad6cebb3365881250d7539d00d03 (diff) | |
Fix CHANGES.
| -rw-r--r-- | CHANGES | 11 |
1 files changed, 7 insertions, 4 deletions
@@ -1,3 +1,10 @@ +Changes from V8.5beta3 +====================== + +Specification language + +- Syntax "$(tactic)$" changed to "ltac:(tactic)". + Changes from V8.5beta2 to V8.5beta3 =================================== @@ -10,10 +17,6 @@ Vernacular commands introducing it. - New command "Show id" to show goal named id. -Specification language - -- Syntax "$(tactic)$" changed to "ltac: tactic". - Tactics - New flag "Regular Subst Tactic" which fixes "subst" in situations where |
