aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts/coqmktop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'scripts/coqmktop.ml')
-rw-r--r--scripts/coqmktop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ffa62cdf4..0723aec67 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -44,7 +44,7 @@ let camlp4objs =
"q_coqast.cmo" ]
let topobjs = camlp4objs
-let gramobjs = ["g_zsyntax.cmo"; "g_natsyntax.cmo"]
+let gramobjs = []
let notopobjs = gramobjs
(* 5. High-level tactics objects *)