diff options
Diffstat (limited to 'mathcomp/ssreflect/ssreflect.v')
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 95da9cd..2925496 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -17,6 +17,15 @@ Global Set Bullet Behavior "None". (* --> Usage: Notation old := (deprecate old new) (only parsing). *) (* --> Caveat: deprecate old new only inherits new's maximal implicits; *) (* on-demand implicits should be added after : (deprecate old new _). *) +(* --> Caveat 2: if premises or conclusions need to be adjusted, of for *) +(* non-prenex implicits, use the idiom: *) +(* Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...) *) +(* _ _ ... _) (only printing). *) +(* where all the implicit a_i's occur first, and correspond to the *) +(* trailing _'s, making sure deprecate old new is fully applied and *) +(* there are _no implicits_ inside the (fun .. => ..) expression. This *) +(* is to avoid triggering a bug in SSReflect elaboration that is *) +(* triggered by such evars under binders. *) (* Import Deprecation.Silent :: turn off deprecation warning messages. *) (* Import Deprecation.Reject :: raise an error instead of only warning. *) (******************************************************************************) |