Merge PR coq#7116: Fixes coq#7110: missing test on the absence of a "…

…as" while looking for a notation for a nested pattern

interp/constrextern.ml

@@ -478,7 +478,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
       if is_inactive_rule keyrule then raise No_match;
       let loc = t.loc in
       match DAst.get t with
-	| PatCstr (cstr,_,na) ->
+        | PatCstr (cstr,args,na) ->
+          let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
 	  let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
 	    (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias ?loc p na

interp/notation_ops.ml

@@ -1335,10 +1335,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
-  | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
+  | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
       let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
       sigma,(0,l)
-  | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
+  | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in

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]

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.