aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/compat.ml4
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-09-15 10:35:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-09-15 10:35:59 +0000
commitda3edaa7eab2bed17cdfb2c455f2e6b5b0318c4d (patch)
tree14b6ae25300dc08c9ca5ff86ad88a78910df7b92 /lib/compat.ml4
parent4f39e160d05b0e5501a909b3041589303651670b (diff)
* 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
Diffstat (limited to 'lib/compat.ml4')
-rw-r--r--lib/compat.ml442
1 files changed, 36 insertions, 6 deletions
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 6fe4c4c7e..40cffadb7 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -6,14 +6,26 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4use: "pa_ifdef.cmo" i*)
+(*i camlp4use: "pa_macro.cmo" i*)
(* Compatibility file depending on ocaml version *)
-(* IFDEF not available in 3.06; use ifdef instead *)
+IFDEF OCAML309 THEN DEFINE OCAML308 END
-(* type loc is different in 3.08 *)
-ifdef OCAML_308 then
+IFDEF CAMLP5 THEN
+module M = struct
+type loc = Stdpp.location
+let dummy_loc = Stdpp.dummy_loc
+let make_loc = Stdpp.make_loc
+let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else Stdpp.encl_loc loc1 loc2
+type token = string*string
+type lexer = token Token.glexer
+let using l x = l.Token.tok_using x
+end
+ELSE IFDEF OCAML308 THEN
module M = struct
type loc = Token.flocation
let dummy_loc = Token.dummy_loc
@@ -26,16 +38,34 @@ let unloc (b,e) =
assert (dummy_loc = (b,e) or make_loc loc = (b,e));
*)
loc
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else (fst loc1, snd loc2)
+type token = Token.t
+type lexer = Token.lexer
+let using l x = l.Token.using x
end
-else
+ELSE
module M = struct
type loc = int * int
let dummy_loc = (0,0)
let make_loc x = x
let unloc x = x
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else (fst loc1, snd loc2)
+type token = Token.t
+type lexer = Token.lexer
+let using l x = l.Token.using x
end
+END
+END
type loc = M.loc
let dummy_loc = M.dummy_loc
-let unloc = M.unloc
let make_loc = M.make_loc
+let unloc = M.unloc
+let join_loc = M.join_loc
+type token = M.token
+type lexer = M.lexer
+let using = M.using