diff options
| author | Emilio Jesus Gallego Arias | 2019-01-23 13:48:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-23 13:48:10 +0100 |
| commit | bc943f0956496ed0e02de08a5a3a1b922423e72c (patch) | |
| tree | f60995b5b53bb543e4f83611bde2b5c47998ed6f /test-suite | |
| parent | 398b13bb6937cca90c685e4f8dba6a1db60a103e (diff) | |
| parent | 03a50923af6fec0deb0c3c2218656bfb74341e47 (diff) | |
Merge PR #9337: Fixing #9329: registering empty levels in the order they are computed
Reviewed-by: ejgallego
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_9329.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v new file mode 100644 index 0000000000..c0322dec40 --- /dev/null +++ b/test-suite/bugs/closed/bug_9329.v @@ -0,0 +1,12 @@ +(* Declare empty levels in the same order they are computed *) + +Notation "< a ; b ; c >1" := + (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21). +Notation "< a ; b ; c >2" := + (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31). +Notation "< a ; b ; c >3" := + (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41). +Notation "< a ; b ; c >4" := + (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49). +Notation "< a ; b >" := + (sum a b) (at level 61, a at level 63, b at level 62). |