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 /vernac | |
| parent | d88f9883ce8313c82cb081987e30de1d7201805e (diff) | |
Fixing #9329 (registering empty levels in the order they are recomputed).
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |