portage en ocaml / camlp4 3.00

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

5 files changed, 28 insertions, 14 deletions

diff --git a/.depend.coq b/.depend.coq
index 06349fb1c2..2446651115 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,7 +1,7 @@
 theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
 theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
-theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v tactics/Equality.vo theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
-theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/g_zsyntax.cmo
+theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo parsing/g_zsyntax.cmo
 theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo
 theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
 theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
@@ -47,10 +47,11 @@ theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
-theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/g_natsyntax.cmo
+theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo parsing/g_natsyntax.cmo
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
 test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
 tactics/Tauto.vo: tactics/Tauto.v
+tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
 tactics/Equality.vo: tactics/Equality.v
 syntax/PPTactic.vo: syntax/PPTactic.v
 syntax/PPConstr.vo: syntax/PPConstr.v
diff --git a/Makefile b/Makefile
index d83cb94acf..9ece34b016 100644
--- a/Makefile
+++ b/Makefile
@@ -41,7 +41,7 @@ OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
 CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE)
 
-COQINCLUDES=-I theories/Init -I theories/Logic -I theories/Arith \
+COQINCLUDES=-I parsing -I theories/Init -I theories/Logic -I theories/Arith \
             -I theories/Bool -I theories/Zarith
 
 ###########################################################################
@@ -361,7 +361,13 @@ tags:
 # lexer (compiled with camlp4 to get optimized streams)
 
 parsing/lexer.cmo: parsing/lexer.ml
-	$(OCAMLC_P4O) -c $<
+	$(OCAMLC) $(BYTEFLAGS) -pp "camlp4o pa_ifdef.cmo" -c $<
+
+parsing/lexer.cmx: parsing/lexer.ml
+	$(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o pa_ifdef.cmo" -c $<
+
+parsing/lexer.cmi: parsing/lexer.mli
+	$(OCAMLC) $(BYTEFLAGS) -pp "camlp4o pa_ifdef.cmo" -c $<
 
 clean::
 	rm -f parsing/lexer.ml
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 721afa2d1c..6c99238f4f 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -15,6 +15,9 @@ val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
 
 val add_token : Token.pattern -> unit
 
+ifdef CAMLP4_300 then
+val tparse : string * string -> ((string * string) Stream.t -> string) option
+else
 val tparse : string * string -> (string * string) Stream.t -> string
 
 val token_text : string * string -> string
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 6a35d19dee..0f7b4938c9 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -261,9 +261,12 @@ let token_text = function
   | (con, prm) -> con ^ " \"" ^ prm ^ "\""
 
 let tparse (p_con, p_prm) =
-  if p_prm = "" then
-    parser [< '(con, prm) when con = p_con >] -> prm
+  ifdef CAMLP4_300 then 
+    None
   else
-    parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
+    if p_prm = "" then
+      parser [< '(con, prm) when con = p_con >] -> prm
+    else
+      parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
 
 }
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 55594d705f..a148c7695c 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -204,7 +204,7 @@ let clean file =
   end
 
 (*Gives all modules in dir. Uses .cmi. Unix again sorry again*)
-let all_modules_in_dir dir=
+let all_modules_in_dir dir =
   try
     let lst = ref []
     and stg = ref ""
@@ -245,15 +245,16 @@ let tmp_dynlink()=
   tmp
 
 (*Initializes the kind of loading in the main program*)
-let declare_loading_string()=
+let declare_loading_string () =
   if !opt then
     "Mltop.set Mltop.Native;;\n"
   else if not !top then
     "Mltop.set Mltop.WithoutTop;;\n"
   else
-    "Mltop.set (Mltop.WithTop {Mltop.load_obj=Topdirs.dir_load;
-                                 Mltop.use_file=Topdirs.dir_use;
-                                 Mltop.add_dir=Topdirs.dir_directory});;\n"
+    "let ppf = Format.std_formatter;;
+     Mltop.set (Mltop.WithTop {Mltop.load_obj=Topdirs.dir_load ppf;
+                               Mltop.use_file=Topdirs.dir_use ppf;
+                               Mltop.add_dir=Topdirs.dir_directory});;\n"
 
 (* create a temporary main file to link *)
 let create_tmp_main_file modules =
@@ -273,7 +274,7 @@ let create_tmp_main_file modules =
       output_string oc "Coqtop.start();;\n";
     (* Start the Ocaml toplevel if it exists *)
     if !top then
-      output_string oc "Printexc.catch Toploop.loop(); exit 1;;\n";
+      output_string oc "Printexc.catch Toploop.loop ppf; exit 1;;\n";
     close_out oc;
     main_name
   with e ->