From 8d80875d230bd8af5611ec04bced1e5a17d058b0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 12:46:42 +0100 Subject: Inherit scopes and implicit sign. in notations for partially applied pattern. Exception: when the notation is to some @id. Formerly, this was ignored for all kinds of string notations. --- test-suite/success/Notations2.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'test-suite') 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 *) -- cgit v1.2.3