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 /vernac | |
| 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 '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 |