Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 34afd2200d..f15ac3d78f 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -19,7 +19,7 @@ open Unix
 (* 1. Core objects *)
 let ocamlobjs = ["unix.cma"]
 let dynobjs = ["dynlink.cma"]
-let camlp4objs = ["gramlib.cma"]
+let camlp4objs = [(*"odyl.cma"; "camlp4.cma";*) "gramlib.cma"]
 let configobjs = ["coq_config.cmo"]
 let libobjs = ocamlobjs @ camlp4objs @ configobjs
 
@@ -34,6 +34,7 @@ let parsing = split_cmo Tolink.parsing
 let proofs = split_cmo Tolink.proofs
 let tactics = split_cmo Tolink.tactics
 let toplevel = split_cmo Tolink.toplevel
+let highparsing = split_cmo Tolink.highparsing
 
 let core_objs = 
   libobjs @ lib @ kernel @ library @ pretyping @ parsing @ 
@@ -44,8 +45,7 @@ let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"]
 
 (* 4. Toplevel objects *)
 let camlp4objs =
-  ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo";
-   "q_coqast.cmo" ]
+  ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ]
 let topobjs = camlp4objs
 
 let gramobjs = []
@@ -92,8 +92,8 @@ let files_to_link userfiles =
   let command_objs = if !searchisos then coqsearch else [] in
   let toplevel_objs = if !top then topobjs else if !opt then notopobjs else []
   in
-  let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ hightactics @
-    toplevel_objs in
+  let objs = core_objs @ dyn_objs @ toplevel @ highparsing @ 
+    command_objs @ hightactics @ toplevel_objs in
   let tolink =
     if !opt then 
       (List.map native_suffix objs) @ userfiles