diff options
Diffstat (limited to 'test-suite/bugs/closed/4785.v')
| -rw-r--r-- | test-suite/bugs/closed/4785.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index 14af2d91df..c3c97d3f59 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -21,7 +21,7 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil : mylist_scope. +Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. |