aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/g_toplevel.mlg
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/g_toplevel.mlg')
-rw-r--r--toplevel/g_toplevel.mlg6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 53d3eef23..5aba3d6b0 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,9 +21,9 @@ type vernac_toplevel =
| VernacControl of vernac_control
module Toplevel_ : sig
- val vernac_toplevel : vernac_toplevel CAst.t Gram.entry
+ val vernac_toplevel : vernac_toplevel CAst.t Entry.t
end = struct
- let gec_vernac s = Gram.entry_create ("toplevel:" ^ s)
+ let gec_vernac s = Entry.create ("toplevel:" ^ s)
let vernac_toplevel = gec_vernac "vernac_toplevel"
end
@@ -49,6 +49,6 @@ END
{
-let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa
+let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa
}