From 03a50923af6fec0deb0c3c2218656bfb74341e47 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Jan 2019 23:24:28 +0100
Subject: Fixing #9329 (registering empty levels in the order they are
 recomputed).

Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
---
 vernac/egramcoq.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3