aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES2
1 files changed, 1 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 050d3e999f..202e27e377 100644
--- a/CHANGES
+++ b/CHANGES
@@ -161,7 +161,7 @@ Specification Language
break user notations using "$(", fixable by inserting a space or
rewriting the notation).
- Constructors in pattern-matching patterns now respect the same rules
- regarding implicit arguments than in applicative position. The old
+ regarding implicit arguments as in applicative position. The old
behavior can be recovered by the command "Set Asymmetric
Patterns". As a side effect, notations for constructors explicitly
mentioning non-implicit parameters can now be used in patterns.