From da3edaa7eab2bed17cdfb2c455f2e6b5b0318c4d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 15 Sep 2007 10:35:59 +0000
Subject: * Adding compability with ocaml 3.10 + camlp5 (rework of   the patch
 by S. Mimram) * for detecting architecture, also look for /bin/uname *
 restore the compatibility of kernel/byterun/coq_interp.c with   ocaml 3.07
 (caml_modify vs. modify). There is still an issue   with this 3.07 and
 64-bits architecture (see coqdev and a future   bug report).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 2 +-
 toplevel/mltop.ml4     | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 855c98f93b..9a162997b6 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -28,7 +28,7 @@ open Notation
 (**********************************************************************)
 (* Tokens                                                             *)
 
-let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
+let cache_token (_,s) = Compat.using Pcoq.lexer ("", s)
 
 let (inToken, outToken) =
   declare_object {(default_object "TOKEN") with
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index c0e090290a..43ab05aa8c 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_ifdef.cmo" i*)
+(*i camlp4use: "pa_macro.cmo" i*)
 (* WARNING
  * camlp4deps will not work for this file unless Makefile system enhanced.
  *)
@@ -103,7 +103,7 @@ let dir_ml_load s =
                 str s; str" to Coq code." >])
 (* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
-      ifdef Byte then
+      IFDEF Byte THEN
 	(* WARNING
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
@@ -117,7 +117,7 @@ let dir_ml_load s =
 	    [Filename.dirname gname]
 	with | Dynlink.Error a ->
           errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
-      else ()
+      ELSE () END
     | Native ->
 	errorlabstrm "Mltop.no_load_object"
           [< str"Loading of ML object file forbidden in a native Coq" >]
-- 
cgit v1.2.3