diff options
| -rw-r--r-- | interp/constrextern.ml | 3 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 16 |
4 files changed, 28 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb5fd5294..7792eff66 100644 --- a/interp/constrextern.ml +++ b/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 diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index a0d69ce79..aa9a6ed0d 100644 --- a/interp/notation_ops.ml +++ b/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 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. |