diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Notations2.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 1b33863e3b..2533a39cc4 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -154,3 +154,14 @@ Module M16. Print Grammar foo. Print Grammar foo2. End M16. + +(* Example showing the need for strong evaluation of + cases_pattern_of_glob_constr (this used to raise Not_found at some + time) *) + +Module M17. + +Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pattern). +Check fun y : nat => # (x,z) ## y & y. + +End M17. |