From 8ad6bf357284f3fcfd94f08561450bb5bf38ad36 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 29 Mar 2018 18:30:50 +0200
Subject: Fixes #7110 ("as" untested while looking for notation for nested
 patterns).

---
 test-suite/output/Notations3.out |  8 ++++++++
 test-suite/output/Notations3.v   | 16 ++++++++++++++++
 2 files changed, 24 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 1987b6a6e..304353f55 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -223,3 +223,11 @@ fun S : nat => [[S | S.S]]
      : Set
 exists2 '{{y, z}} : nat * nat, y > z & z > y
      : Prop
+foo = 
+fun l : list nat => match l with
+                    | _ :: (_ :: _) as l1 => l1
+                    | _ => l
+                    end
+     : list nat -> list nat
+
+Argument scope is [list_scope]
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index c165f9553..d2d136946 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -278,10 +278,12 @@ Set Printing Notations.
 
 (* Check insensitivity of "match" clauses to order *)
 
+Module IfPat.
 Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
   (match t with S n => p | 0 => q end)
   (at level 200).
 Check fun x => if x is n.+1 then n else 1.
+End IfPat.
 
 (* Examples with binding patterns *)
 
@@ -338,11 +340,13 @@ Check ∀ '(((x,y),true)|((x,y),false)), x>y.
 
 (* Check Georges' printability of a "if is then else" notation *)
 
+Module IfPat2.
 Notation "'if' c 'is' p 'then' u 'else' v" :=
   (match c with p => u | _ => v end)
   (at level 200, p pattern at level 100).
 Check fun p => if p is S n then n else 0.
 Check fun p => if p is Lt then 1 else 0.
+End IfPat2.
 
 (* Check that mixed binders and terms defaults to ident and not pattern *)
 Module F.
@@ -364,3 +368,15 @@ Check {'(x,y)|x+y=0}.
 
 (* Check exists2 with a pattern *)
 Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
+
+Module Issue7110.
+Open Scope list_scope.
+Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
+  (at level 0).
+Definition foo (l : list nat) :=
+  match l with
+  | a :: (b :: l) as l1 => l1
+  | _ => l
+end.
+Print foo.
+End Issue7110.
-- 
cgit v1.2.3