diff options
| author | Hugo Herbelin | 2019-01-10 23:24:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-01-22 15:09:08 +0100 |
| commit | 03a50923af6fec0deb0c3c2218656bfb74341e47 (patch) | |
| tree | fef135ed428ef0851234e9066ccd05a1bd83d96b | |
| parent | d88f9883ce8313c82cb081987e30de1d7201805e (diff) | |
Fixing #9329 (registering empty levels in the order they are recomputed).
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
| -rw-r--r-- | test-suite/bugs/closed/bug_9329.v | 12 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 3 |
2 files changed, 14 insertions, 1 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). diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 43abc0a200..1a07d74a0e 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -146,7 +146,8 @@ let register_empty_levels accu forpat levels = (where, ans) :: rem, save_levels accu where nlev else rem, accu in - filter accu levels + let (l,accu) = filter accu levels in + List.rev l, accu let find_position accu custom forpat assoc level = let accu, (clev, plev) = find_levels accu custom in |