diff options
| -rw-r--r-- | interp/constrintern.ml | 12 | ||||
| -rw-r--r-- | test-suite/success/Notations2.v | 6 |
2 files changed, 13 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1149cf1f58..1b9b45c3fb 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1680,7 +1680,7 @@ let drop_notations_pattern looked_for genv = test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; let (_,argscs) = find_remaining_scopes [] pats g in - Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) + Some (g,[],List.map2 (in_pat_sc scopes) argscs pats) with Not_found -> None and in_pat top scopes pt = let open CAst in @@ -1780,7 +1780,15 @@ let drop_notations_pattern looked_for genv = let (argscs1,argscs2) = find_remaining_scopes pl args g in let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in let pl = add_local_defs_and_check_length loc genv g pl args in - DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) + let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in + let pat = + if List.length pl = 0 then + (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then + implicit arguments are not inherited *) + RCPatCstr (g, pl @ args, []) + else + RCPatCstr (g, pl, args) in + DAst.make ?loc @@ pat | NList (x,y,iter,terminator,revert) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index dca0208fb0..f166a53256 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -66,14 +66,14 @@ Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 Notation "# x" := (pair' x) (at level 0, x at level 1). Check pair' 0 0 0 : prod' bool bool. Check # 0 0 0 : prod' bool bool. -Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end. +Check fun A (x :prod' bool A) => match x with # 0 y 0 => 2 | _ => 1 end. (* 6. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *) Notation "## x" := ((@pair') _ x) (at level 0, x at level 1). Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. Check ## 0%bool 0 0 : prod' bool bool. -Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end. +Check fun A (x :prod' bool A) => match x with ## 0%bool y 0 => 2 | _ => 1 end. (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *) Notation "###" := (@pair') (at level 0). @@ -89,7 +89,7 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. (* 9. Non-@id notations inherit implicit arguments and scopes *) Notation "##### x" := (pair' x) (at level 0, x at level 1). Check ##### 0 0 0 : prod' bool bool. -Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. +Check fun A (x :prod' bool A) => match x with ##### 0 y 0 => 2 | _ => 1 end. (* 10. Check computation of binding variable through other notations *) (* it should be detected as binding variable and the scopes not being checked *) |