diff options
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -163,10 +163,11 @@ Specification Language - Constructors in pattern-matching patterns now respect the same rules regarding implicit arguments than in applicative position. The old behavior can be recovered by the command "Set Asymmetric - Patterns". As a side effect, Much more notations can be used in - patterns. Considering that the pattern language is rich enough like - that, definitions are now always forbidden in patterns. (source of - incompatibilities for definitions that delta-reduce to a constructor) + Patterns". As a side effect, notations for constructors explicitly + mentioning non-implicit parameters can now be used in patterns. + Considering that the pattern language is already rich enough, binding + local definitions is however now forbidden in patterns (source of + incompatibilities for local definitions that delta-reduce to a constructor). - Type inference algorithm now granting opacity of constants. This might also affect behavior of tactics (source of incompatibilities, solvable by re-declaring transparent constants which were set opaque). |