diff options
| author | Matthieu Sozeau | 2016-06-15 15:24:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 56219d80edc91eeab1a8165db87b565165b7e810 (patch) | |
| tree | a1d6cf05e101c52a521b7a9ebf86845d60818f61 | |
| parent | 27d169e82ed3068e6119ff0548f3b6e93854a6bc (diff) | |
Fix wrong tabulation in CHANGES
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -32,7 +32,7 @@ Tactics Hints - Revised the syntax of [Hint Cut] to follow standard notation for regexps. -- Hint Mode now accepts "!" which means that the mode matches only if the +- Hint Mode now accepts "!" which means that the mode matches only if the argument's head is not an evar (it goes under applications, casts, and scrutinees of matches and projections). |