diff options
| -rw-r--r-- | CHANGES | 11 |
1 files changed, 10 insertions, 1 deletions
@@ -40,6 +40,15 @@ Tactics - Tactics and tactic notations now understand the `deprecated` attribute. +Standard Library + +- Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them, + and proved some lemmas about them. Note that this might cause + incompatibilities if you have, e.g., string_scope and Z_scope both + open with string_scope on top, and expect `=?` to refer to `Z.eqb`. + Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you + want). + Tools - Coq_makefile lets one override or extend the following variables from @@ -99,7 +108,7 @@ SSReflect In particular rule 3 lets one write {x}/v even if v uses the variable x: indeed the view is executed before the renaming. -- An empty clear switch is now accepted in intro patterns before a +- An empty clear switch is now accepted in intro patterns before a view application whenever the view is a variable. One can now write {}/v to mean {v}/v. Remark that {}/x is very similar to the idiom {}e for the rewrite tactic (the equation e is used for |