diff options
Diffstat (limited to 'test-suite/success/Notations.v')
| -rw-r--r-- | test-suite/success/Notations.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 89f11059..2371d32c 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -96,3 +96,8 @@ Notation "'FORALL' x .. y , P" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity) : type_scope. Fail Check fun x => match x with S (FORALL x, _) => 0 end. + +(* Bug #2708: don't check for scope of variables used as binder *) + +Parameter traverse : (nat -> unit) -> (nat -> unit). +Notation traverse_var f l := (traverse (fun l => f l) l). |