aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorfilliatr2000-10-27 08:46:13 +0000
committerfilliatr2000-10-27 08:46:13 +0000
commit751620c70bd3a77ed8fde7cca9e3893f339643b3 (patch)
tree517f1e98436989ba549f36f4c895624482e1419e /scripts
parentfc6300ffd9d98da50b6302e11742ac29eb572366 (diff)
g_natsyntax et g_zsyntax maintenant toujours linkes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ffa62cdf4a..0723aec671 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 *)