aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/g_toplevel.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4
index d5d558b9b..e3cefe236 100644
--- a/toplevel/g_toplevel.ml4
+++ b/toplevel/g_toplevel.ml4
@@ -35,7 +35,7 @@ GEXTEND Gram
| IDENT "Quit"; "." -> CAst.make VernacQuit
| IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
CAst.make (VernacBacktrack (n,m,p))
- | cmd = main_entry ->
+ | cmd = Pvernac.main_entry ->
match cmd with
| None -> raise Stm.End_of_input
| Some (loc,c) -> CAst.make ~loc (VernacControl c)