diff options
| author | Emilio Jesus Gallego Arias | 2019-05-24 00:45:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-24 00:45:40 +0200 |
| commit | 48bda9d680f605f012eb9c3af61f9e076a7d51be (patch) | |
| tree | 6d86a4ed1f3f5d54aeeaf9e55d35d9d3813496bc /test-suite | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
| parent | 7c82a2713c8827ebc1e2896c83c6e7bd2f81c063 (diff) | |
Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Case18.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v index be9ca8d41b..6bea435090 100644 --- a/test-suite/success/Case18.v +++ b/test-suite/success/Case18.v @@ -1,7 +1,10 @@ (* Check or-patterns *) +(* Non-interference with Numbers divisibility. *) +Reserved Notation "( p | q )" (at level 0). + Definition g x := - match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end. + match x with ((((1 as x),_) | (_,x)), ((_,(2 as y)) | (y,_))) => (x,y) end. Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)). |