Port g_toplevel to the homebrew GEXTEND parser.

1 files changed, 13 insertions, 6 deletions

diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.mlg
index e3cefe236..53d3eef23 100644
--- a/toplevel/g_toplevel.ml4
+++ b/toplevel/g_toplevel.mlg
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
 open Pcoq
 open Pcoq.Prim
 open Vernacexpr
@@ -28,20 +29,26 @@ end
 
 open Toplevel_
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL: vernac_toplevel;
   vernac_toplevel: FIRST
-    [ [ IDENT "Drop"; "." -> CAst.make VernacDrop
-      | IDENT "Quit"; "." -> CAst.make VernacQuit
+    [ [ IDENT "Drop"; "." -> { CAst.make VernacDrop }
+      | IDENT "Quit"; "." -> { CAst.make VernacQuit }
       | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
-        CAst.make (VernacBacktrack (n,m,p))
+        { CAst.make (VernacBacktrack (n,m,p)) }
       | cmd = Pvernac.main_entry ->
-              match cmd with
+              { match cmd with
               | None -> raise Stm.End_of_input
-              | Some (loc,c) -> CAst.make ~loc (VernacControl c)
+              | Some (loc,c) -> CAst.make ~loc (VernacControl c) }
       ]
     ]
   ;
 END
 
+{
+
 let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa
+
+}