Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.

This is because it can raise Not_found in depth and we need to catch
it at the right time.

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.