diff options
Diffstat (limited to 'toplevel/g_toplevel.mlg')
| -rw-r--r-- | toplevel/g_toplevel.mlg | 10 |
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) } ] ] ; |