the following had to be adapted ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' lib/pp.ml4` -impl" -c -impl lib/pp.ml4 [tmp] ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -c library/goptions.ml ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/lexer.ml4` pr_o.cmo -impl" -c -impl parsing/lexer.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/pcoq.ml4` -impl" -c -impl parsing/pcoq.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_prim.ml4` -impl" -c -impl parsing/g_prim.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_proofs.ml4` -impl" -c -impl parsing/g_proofs.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_basevernac.ml4` -impl" -c -impl parsing/g_basevernac.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_vernac.ml4` -impl" -c -impl parsing/g_vernac.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_tactic.ml4` -impl" -c -impl parsing/g_tactic.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_ltac.ml4` -impl" -c -impl parsing/g_ltac.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_constr.ml4` -impl" -c -impl parsing/g_constr.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_cases.ml4` -impl" -c -impl parsing/g_cases.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/g_module.ml4` -impl" -c -impl parsing/g_module.ml4 #--- ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/q_util.ml4` -impl" -c -impl parsing/q_util.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/q_coqast.ml4` -impl" -c -impl parsing/q_coqast.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/argextend.ml4` -impl" -c -impl parsing/argextend.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/tacextend.ml4` -impl" -c -impl parsing/tacextend.ml4 ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' parsing/vernacextend.ml4` -impl" -c -impl parsing/vernacextend.ml4 #--- ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/bignat.cmo lib/dyn.cmo lib/options.cmo lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo kernel/declarations.cmo kernel/environ.cmo library/nameops.cmo library/libnames.cmo library/summary.cmo library/nametab.cmo library/libobject.cmo library/lib.cmo library/goptions.cmo library/decl_kinds.cmo pretyping/rawterm.cmo pretyping/pattern.cmo pretyping/evd.cmo interp/topconstr.cmo interp/genarg.cmo interp/ppextend.cmo parsing/coqast.cmo parsing/ast.cmo proofs/tacexpr.cmo parsing/ast.cmo parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_coqast.cmo parsing/egrammar.cmo parsing/argextend.cmo parsing/tacextend.cmo parsing/vernacextend.cmo parsing/g_prim.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo -linkall -a -o parsing/grammar.cma ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -pp "camlp4o -I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$|\1|p' tactics/extraargs.ml4` -impl" -c -impl tactics/extraargs.ml4 ------ starts with coq@bovmas:~/profile$ make world ocamlcp -p a -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -c config/coq_config.mli ocamlcp -p a -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I translate -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I contrib/linear -I contrib/funind -I contrib/first-order -I /usr/lib/ocaml/3.06/camlp4 -g -c config/coq_config.ml