diff options
| author | coqbot-app[bot] | 2020-09-23 13:32:10 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-23 13:32:10 +0000 |
| commit | d9d89ad43e62cfd1dfd3beed924f82d3de7bcc23 (patch) | |
| tree | ff49b24319d33e24930433e57ecc521fa99f0dfe /test-suite | |
| parent | bb6e78ef2ca4bf0d686654fa3f66dd780f5be0ac (diff) | |
| parent | c55f520032492ac203a0533c88ecc6c850217be0 (diff) | |
Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)
Reviewed-by: ejgallego
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/bug_13018.out | 14 | ||||
| -rw-r--r-- | test-suite/output/bug_13018.v | 30 |
2 files changed, 44 insertions, 0 deletions
diff --git a/test-suite/output/bug_13018.out b/test-suite/output/bug_13018.out new file mode 100644 index 0000000000..2f60409e23 --- /dev/null +++ b/test-suite/output/bug_13018.out @@ -0,0 +1,14 @@ +gargs:( (!) ) + : list nat +gargs:( (!, !, !) ) + : list nat +OnlyGargs[ (!) ] + : list nat +gargs999:( (!) ) + : list nat +gargs999:( (!, !, !) ) + : list nat +OnlyGargs[ (!) ] + : list nat +OnlyGargs999[ (!) ] + : list nat diff --git a/test-suite/output/bug_13018.v b/test-suite/output/bug_13018.v new file mode 100644 index 0000000000..3fb8b7f905 --- /dev/null +++ b/test-suite/output/bug_13018.v @@ -0,0 +1,30 @@ +Undelimit Scope list_scope. +Declare Custom Entry gnat. +Declare Custom Entry gargs. + +Notation "!" := 42 (in custom gnat). +Notation "gargs:( e )" := e (e custom gargs). +Notation "( x )" := (cons x (@nil nat)) (in custom gargs, x custom gnat). +Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..)) + (in custom gargs, x custom gnat, y custom gnat, z custom gnat). + +Check gargs:( (!) ). (* cons 42 nil *) +Check gargs:( (!, !, !) ). (* cons 42 (42 :: 42 :: nil) *) + +Definition OnlyGargs {T} (x:T) := x. +Notation "OnlyGargs[ x ]" := (OnlyGargs x) (at level 10, x custom gargs). +Check OnlyGargs[ (!) ]. (* OnlyGargs[ cons 42 nil] *) + +Declare Custom Entry gargs999. +Notation "gargs999:( e )" := e (e custom gargs999 at level 999). +Notation "( x )" := (cons x (@nil nat)) (in custom gargs999, x custom gnat at level 999). +Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..)) + (in custom gargs999, x custom gnat at level 999, y custom gnat at level 999, z custom gnat at level 999). + +Check gargs999:( (!) ). (* gargs999:( (!)) *) +Check gargs999:( (!, !, !) ). (* gargs999:( (!, !, !)) *) +Check OnlyGargs[ (!) ]. (* OnlyGargs[ gargs999:( (!))] *) + +Definition OnlyGargs999 {T} (x:T) := x. +Notation "OnlyGargs999[ x ]" := (OnlyGargs999 x) (at level 10, x custom gargs999 at level 999). +Check OnlyGargs999[ (!) ]. (* OnlyGargs999[ (!)] *) |