[vernac] [ast] Make location info an attribute of vernaculars.

This has been a mess for quite a while, we try to improve it.

1 files changed, 5 insertions, 5 deletions

diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index f2025858d7..0cac024300 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,7 +21,7 @@ type vernac_toplevel =
   | VernacControl of vernac_control
 
 module Toplevel_ : sig
-  val vernac_toplevel : vernac_toplevel CAst.t option Entry.t
+  val vernac_toplevel : vernac_toplevel option Entry.t
 end = struct
   let gec_vernac s = Entry.create ("toplevel:" ^ s)
   let vernac_toplevel = gec_vernac "vernac_toplevel"
@@ -34,14 +34,14 @@ open Toplevel_
 GRAMMAR EXTEND Gram
   GLOBAL: vernac_toplevel;
   vernac_toplevel: FIRST
-    [ [ IDENT "Drop"; "." -> { Some (CAst.make VernacDrop) }
-      | IDENT "Quit"; "." -> { Some (CAst.make VernacQuit) }
+    [ [ IDENT "Drop"; "." -> { Some VernacDrop }
+      | IDENT "Quit"; "." -> { Some VernacQuit }
       | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
-        { Some (CAst.make (VernacBacktrack (n,m,p))) }
+        { Some (VernacBacktrack (n,m,p)) }
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None
-              | Some {CAst.loc; v} -> Some (CAst.make ?loc (VernacControl v)) }
+              | Some v -> Some (VernacControl v) }
       ]
     ]
   ;