aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 9220605e85..99fa8f6eba 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -45,8 +45,7 @@ let camlp4topobjs =
[ "Camlp4Top.cmo";
"Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
"Camlp4Parsers/Camlp4OCamlParser.cmo";
- "Camlp4Parsers/Camlp4GrammarParser.cmo";
- "grammar/q_util.cmo"; "grammar/q_coqast.cmo" ]
+ "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
let topobjs = camlp4topobjs
let gramobjs = []