Ide: more reorganisation and cleanup

 - Avoid using Util which depends on Compat and hence Camlp4
 - Instead, a small Minilib module specific to coqide, which
   duplicate 5 functions from Util (50 lines)
 - some dead code removal
 - the coqlib variable is asked to coqtop
 - remove obsolete Util.check_for_interrupt

 This way, coqide only depends on 3 files outside ide/ :
 Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted
 accordingly.

TODO: how should we signal coqide error, warnings, etc ?
 For the moment, some Printf.eprintf, some failwith.
 To uniformize later...

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

17 files changed, 137 insertions, 74 deletions

diff --git a/Makefile.build b/Makefile.build
index 529238d674..eefafb0cb2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -313,16 +313,16 @@ coqide-byte: $(COQIDEBYTE) $(COQIDE)
 coqide-opt:  $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
 coqide-files: $(IDEFILES)
 
-$(COQIDEOPT): $(LINKIDEOPT) $(LIBCOQRUN) $(COQTOPOPT)
+$(COQIDEOPT): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa\
-		 gtkThread.cmx dynlink.cmxa str.cmxa $(CAMLP4MOD).cmxa $(LIBCOQRUN) $(LINKIDEOPT)
+		 gtkThread.cmx str.cmxa $(LINKIDEOPT)
 	$(STRIP) $@
 
-$(COQIDEBYTE): $(LINKIDE) $(LIBCOQRUN) $(COQTOPBYTE)
+$(COQIDEBYTE): $(LINKIDE)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\
-		dynlink.cma str.cma $(CAMLP4MOD).cma $(COQRUNBYTEFLAGS) $(LIBCOQRUN) $(LINKIDE)
+		str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)
 
 $(COQIDE):
 	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
diff --git a/Makefile.common b/Makefile.common
index c51ca4011a..ce99603fee 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -217,15 +217,11 @@ INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS))
 LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
-LIBCMA:=lib/lib.cma
+IDEDEPS:=$(CONFIG) lib/flags.cmo toplevel/ide_intf.cmo
 IDECMA:=ide/ide.cma
-IDEINTF:=toplevel/ide_intf.cmo
 
-IDELIBS:=$(CONFIG) $(LIBCMA) $(IDEINTF) $(IDECMA)
-IDELIBSOPT:=$(subst .cmo,.cmx,$(IDELIBS:.cma=.cmxa))
-
-LINKIDE:=$(IDELIBS) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTDEPS) $(IDELIBSOPT) ide/coqide_main_opt.ml
+LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEDEPS:.cmo=.cmx) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml
 
 # modules known by the toplevel of Coq
 
diff --git a/_tags b/_tags
index dafce3b300..e6ac5e6d0a 100644
--- a/_tags
+++ b/_tags
@@ -8,7 +8,7 @@
 <tools/coq_tex.{native,byte}> : use_str
 <tools/coq_makefile.{native,byte}> : use_str
 <tools/coqdoc/main.{native,byte}> : use_str
-<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide, use_dynlink, use_camlp4, use_libcoqrun
+<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide
 <checker/main.{native,byte}> : use_str, use_unix, use_dynlink, use_camlp4
 <plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
 
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 8d9ede0787..1aaf2b71a4 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -11,7 +11,7 @@
   open Lexing
   open Format
   open Config_parser
-  open Util
+  open Minilib
 
   let string_buffer = Buffer.create 1024
 
diff --git a/ide/config_parser.mly b/ide/config_parser.mly
index 8c414d3880..4ab6950b72 100644
--- a/ide/config_parser.mly
+++ b/ide/config_parser.mly
@@ -9,14 +9,14 @@
 %{
 
   open Parsing
-  open Util
+  open Minilib
 
 %}
 
 %token <string> IDENT STRING
 %token EQUAL EOF
 
-%type <(string list) Util.Stringmap.t> prefs
+%type <(string list) Minilib.Stringmap.t> prefs
 %start prefs
 
 %%
diff --git a/ide/coq.ml b/ide/coq.ml
index 96048c3b30..b1bb1f1831 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,9 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
-open Compat
-open Pp
 open Ideutils
 
 type coqtop = {
@@ -21,18 +18,6 @@ type coqtop = {
 
 let prerr_endline s = if !debug then prerr_endline s else ()
 
-let output = ref (Format.formatter_of_out_channel stdout)
-
-let msg m =
-  let b =  Buffer.create 103 in
-  Pp.msg_with (Format.formatter_of_buffer b) m;
-  Buffer.contents b
-
-let msgnl m =
-  (msg m)^"\n"
-
-let i = ref 0
-
 let get_version_date () =
   let date =
     if Glib.Utf8.validate Coq_config.date
@@ -77,7 +62,8 @@ let coqtop_path () =
 
 let filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let oc,ic,ec = Unix.open_process_full (coqtop_path () ^" -nois -filteropts "^argstr) (Unix.environment ()) in
+  let cmd = coqtop_path () ^" -nois -filteropts " ^ argstr in
+  let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
   let filtered_args = read_all_lines oc in
   let message = read_all_lines ec in
   match Unix.close_process_full (oc,ic,ec) with
@@ -102,6 +88,16 @@ let check_connection args =
       List.iter Pervasives.prerr_endline lines;
       exit 1
 
+(* TODO: we can probably merge check_connection () and coqlib () *)
+
+let coqlib () =
+  try
+    let ic = Unix.open_process_in (coqtop_path () ^" -where") in
+    let str = input_line ic in
+    ignore (Unix.close_process_in ic);
+    str
+  with _ -> failwith "Error while reading coqlib from coqtop"
+
 let eval_call coqtop (c:'a Ide_intf.call) =
   Marshal.to_channel coqtop.cin c [];
   flush coqtop.cin;
diff --git a/ide/coq.mli b/ide/coq.mli
index 148840be26..37c5bcd006 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -10,6 +10,7 @@ val short_version : unit -> string
 val version : unit -> string
 val filter_coq_opts : string list -> bool * string list
 val check_connection : string list -> unit
+val coqlib : unit -> string
 
 type coqtop
 
@@ -56,5 +57,3 @@ val make_cases : coqtop -> string -> string list list Ide_intf.value
 val current_status : coqtop -> string Ide_intf.value
 
 val goals : coqtop -> Ide_intf.goals Ide_intf.value
-
-val msgnl : Pp.std_ppcmds -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e553ca0b46..1bb3088538 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Preferences
-open Vernacexpr
 open Coq
 open Coq.PrintOpt
 open Gtk_parsing
@@ -1003,7 +1002,7 @@ object(self)
         (try
            while ((stop#compare (get_current())>=0)
            && (self#process_next_phrase false false false))
-           do Util.check_for_interrupt () done
+           do () (* TODO: this looks obsolete : Util.check_for_interrupt ()*) done
          with Sys.Break ->
            prerr_endline "Interrupted during process_until_iter_or_error");
         sync (fun _ ->
@@ -1185,7 +1184,7 @@ object(self)
     act_id <- Some
                 (input_view#event#connect#key_press ~callback:self#active_keypress_handler);
     prerr_endline "CONNECTED active : ";
-    print_id (Option.get act_id);
+    print_id (match act_id with Some x -> x | None -> assert false);
     match
       filename
     with
@@ -1562,7 +1561,7 @@ let do_print session =
       |Some f_name ->  begin
       let cmd =
         "cd " ^ Filename.quote (Filename.dirname f_name) ^ "; " ^
-        !current.cmd_coqdoc ^ "--coqlib_path " ^Envars.coqlib () ^
+        !current.cmd_coqdoc ^ "--coqlib_path " ^ !Minilib.coqlib ^
 	  " -ps " ^ Filename.quote (Filename.basename f_name) ^
         " | " ^ !current.cmd_print
       in
@@ -1588,7 +1587,7 @@ let load_file handler f =
       let f = absolute_filename f in
       try
         prerr_endline "Loading file starts";
-        if not (Util.list_fold_left_i
+        if not (Minilib.list_fold_left_i
                   (fun i found x -> if found then found else
                      let {analyzed_view=av} = x in
                      (match av#filename with
@@ -1824,7 +1823,7 @@ let main files =
             in
             let cmd =
               "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
-              !current.cmd_coqdoc ^ "--coqlib_path " ^Envars.coqlib () ^ " --" ^ kind ^ 
+              !current.cmd_coqdoc ^ "--coqlib_path " ^ !Minilib.coqlib ^ " --" ^ kind ^
 		" -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
             in
             let s,_ = run_command av#insert_message cmd in
@@ -2199,7 +2198,7 @@ let main files =
 				       | None -> warning "Call to external editor available only on named files"
 				       | Some f ->
 					   save_f ();
-					   let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
+					   let com = Minilib.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
 					   let _ = run_command av#insert_message com in
 					     av#revert)
 			    in
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 4bb80f4a79..4db3ba1436 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -16,10 +16,11 @@ let () =
   let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
   Coqide.sup_args := List.map Filename.quote args;
   Coq.check_connection !Coqide.sup_args;
+  Minilib.coqlib := Coq.coqlib ();
   Coqide.ignore_break ();
     GtkMain.Rc.add_default_file (Ideutils.lib_ide_file ".coqide-gtk2rc");
     (try
-	 GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
+	 GtkMain.Rc.add_default_file (Filename.concat Minilib.home ".coqide-gtk2rc");
      with Not_found -> ());
     ignore (GtkMain.Main.init ());
     initmac () ;
@@ -30,7 +31,7 @@ let () =
 								 `WARNING;`CRITICAL]
 	       (fun ~level msg ->
 		  if level land Glib.Message.log_level `WARNING <> 0
-		  then Pp.warning msg
+		  then Printf.eprintf "Warning: %s\n" msg
 		  else failwith ("Coqide internal error: " ^ msg)));
     Coqide.main files;
     if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ());
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 87b66babae..4861f61e6c 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -1,3 +1,4 @@
+Minilib
 Okey
 Config_file
 Configwin_keys
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 701203061f..783ade6048 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -69,7 +69,7 @@ let mode_tactic sel_cb (proof:GText.view) = function
       proof#buffer#insert head_str;
       List.iter insert_hyp hyps;
       insert_goal cur_goal cur_goal_menu 1 goals_cnt;
-      Util.list_fold_left_i (fun i _ (_,(g,_)) -> insert_goal g [] i goals_cnt) 2 () rem_goals;
+      Minilib.list_fold_left_i (fun i _ (_,(g,_)) -> insert_goal g [] i goals_cnt) 2 () rem_goals;
       ignore(proof#buffer#place_cursor  
         ~where:((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2)));
       ignore(proof#scroll_to_mark `INSERT)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 319cf4e4d2..a4126ae33d 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,8 +37,7 @@ let prerr_string s =
   if !debug then (prerr_string s;flush stderr)
 
 let lib_ide_file f =
-  let coqlib = Envars.coqlib () in
-  Filename.concat (Filename.concat coqlib "ide") f
+  Filename.concat (Filename.concat !Minilib.coqlib "ide") f
 
 let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
 
@@ -284,7 +283,7 @@ let run_command f c =
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
 let browse f url =
-  let com = Flags.subst_command_placeholder !current.cmd_browse url in
+  let com = Minilib.subst_command_placeholder !current.cmd_browse url in
   let s = Sys.command com in
   if s = 127 then
     f ("Could not execute\n\""^com^
diff --git a/ide/minilib.ml b/ide/minilib.ml
new file mode 100644
index 0000000000..b791d779ca
--- /dev/null
+++ b/ide/minilib.ml
@@ -0,0 +1,63 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** Some excerpt of Util and similar files to avoid loading the whole
+    module and its dependencies (and hence Compat and Camlp4) *)
+
+module Stringmap = Map.Make(String)
+
+let list_fold_left_i f =
+  let rec it_list_f i a = function
+    | [] -> a
+    | b::l -> it_list_f (i+1) (f i a b) l
+  in
+  it_list_f
+
+(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that
+   [l1++l2=l] and [l1] has length [i].
+   It raises [Failure] when [i] is negative or greater than the length of [l]  *)
+
+let list_chop n l =
+  let rec chop_aux i acc = function
+    | tl when i=0 -> (List.rev acc, tl)
+    | h::t -> chop_aux (pred i) (h::acc) t
+    | [] -> failwith "list_chop"
+  in
+  chop_aux n [] l
+
+
+let list_map_i f =
+  let rec map_i_rec i = function
+    | [] -> []
+    | x::l -> let v = f i x in v :: map_i_rec (i+1) l
+  in
+  map_i_rec
+
+
+let list_index x =
+  let rec index_x n = function
+    | y::l -> if x = y then n else index_x (succ n) l
+    | [] -> raise Not_found
+  in
+  index_x 1
+
+let list_index0 x l = list_index x l - 1
+
+let list_filter_i p =
+  let rec filter_i_rec i = function
+    | [] -> []
+    | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
+  in
+  filter_i_rec 0
+
+let subst_command_placeholder s t =
+  Str.global_replace (Str.regexp_string "%s") s t
+
+let home = try Sys.getenv "HOME" with Not_found -> "."
+
+let coqlib = ref ""
diff --git a/ide/minilib.mli b/ide/minilib.mli
new file mode 100644
index 0000000000..aac3e3d77d
--- /dev/null
+++ b/ide/minilib.mli
@@ -0,0 +1,24 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** Some excerpts of Util and similar files to avoid depending on them
+    and hence on Compat and Camlp4 *)
+
+module Stringmap : Map.S with type key = string
+
+val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
+val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+val list_filter_i : (int -> 'a -> bool) -> 'a list -> 'a list
+val list_chop : int -> 'a list -> 'a list * 'a list
+val list_index0 : 'a -> 'a list -> int
+
+val subst_command_placeholder : string -> string -> string
+
+val home : string
+
+val coqlib : string ref
diff --git a/ide/preferences.ml b/ide/preferences.ml
index a6aaef2576..e31a5904af 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -8,11 +8,10 @@
 
 open Configwin
 open Printf
-open Util
 
-let pref_file = Filename.concat System.home ".coqiderc"
+let pref_file = Filename.concat Minilib.home ".coqiderc"
 
-let accel_file = Filename.concat System.home ".coqide.keys"
+let accel_file = Filename.concat Minilib.home ".coqide.keys"
 
 let mod_to_str (m:Gdk.Tags.modifier) =
   match m with
@@ -170,9 +169,9 @@ let save_pref () =
   with _ -> ());
   let p = !current in
   try
-    let add = Stringmap.add in
+    let add = Minilib.Stringmap.add in
     let (++) x f = f x in
-    Stringmap.empty ++
+    Minilib.Stringmap.empty ++
     add "cmd_coqc" [p.cmd_coqc] ++
     add "cmd_make" [p.cmd_make] ++
     add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
@@ -228,7 +227,7 @@ let load_pref () =
   try
     let m = Config_lexer.load_file pref_file in
     let np = { p with cmd_coqc = p.cmd_coqc } in
-    let set k f = try let v = Stringmap.find k m in f v with _ -> () in
+    let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in
     let set_hd k f = set k (fun v -> f (List.hd v)) in
     let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
     let set_int k f = set_hd k (fun v -> f (int_of_string v)) in
@@ -295,14 +294,6 @@ let load_pref () =
     prerr_endline ("Could not load preferences ("^
 		   (Printexc.to_string e)^").")
 
-let split_string_format s =
-  try
-    let i = Util.string_index_from s 0 "%s" in
-    let pre = (String.sub s 0 i) in
-    let post = String.sub s (i+2) (String.length s - i - 2) in
-    pre,post
-  with Not_found -> s,""
-
 let configure ?(apply=(fun () -> ())) () =
   let cmd_coqc =
     string
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index 048cc6e24a..499d56bd9a 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -16,14 +16,14 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#append_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Minilib.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 (* XXX - Temporary hack to compile with archaic lablgtk
   method insert_term ?(build=default_build) ?pos (term:'a) =
     let tab_label,menu_label,page = build term in
     let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Minilib.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
  *)
@@ -32,26 +32,26 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#prepend_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Minilib.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 
   method set_term (term:'a) =
     let tab_label,menu_label,page = make_page term in
     let real_pos = super#current_page in
-      term_list <- Util.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
+      term_list <- Minilib.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
       super#set_page ?tab_label ?menu_label page
 
   method get_nth_term i =
     List.nth term_list i
 
   method term_num p =
-    Util.list_index0 p term_list
+    Minilib.list_index0 p term_list
 
   method pages = term_list
 
   method remove_page index =
-    term_list <- Util.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
+    term_list <- Minilib.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
     super#remove_page index
 
   method current_term =
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 6a7d18ebf7..8565c1482b 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -112,10 +112,6 @@ let core_cma = List.map (fun s -> s^".cma") core_libs
 let core_cmxa = List.map (fun s -> s^".cmxa") core_libs
 let core_mllib = List.map (fun s -> s^".mllib") core_libs
 
-let ide_cma = "ide/ide.cma"
-let ide_cmxa = "ide/ide.cmxa"
-let ide_mllib = "ide/ide.mllib"
-
 let tolink = "scripts/tolink.ml"
 
 let c_headers_base =
@@ -371,16 +367,14 @@ let extra_rules () = begin
 
 (** Generation of tolink.ml *)
 
-  rule tolink ~deps:(ide_mllib::core_mllib) ~prod:tolink
+  rule tolink ~deps:core_mllib ~prod:tolink
     (fun _ _ ->
        let cat s = String.concat " " (string_list_of_file s) in
        let core_mods = String.concat " " (List.map cat core_mllib) in
-       let ide_mods = cat ide_mllib in
        let core_cmas = String.concat " " core_cma in
        Echo (["let copts = \"-cclib -lcoqrun\"\n";
 	      "let core_libs = \"coq_config.cmo "^core_cmas^"\"\n";
-	      "let core_objs = \"Coq_config "^core_mods^"\"\n";
-	      "let ide = \""^ide_mods^"\"\n"],
+	      "let core_objs = \"Coq_config "^core_mods^"\"\n"],
 	     tolink));
 
 (** Coqtop *)