diff options
| author | letouzey | 2007-09-15 10:35:59 +0000 |
|---|---|---|
| committer | letouzey | 2007-09-15 10:35:59 +0000 |
| commit | da3edaa7eab2bed17cdfb2c455f2e6b5b0318c4d (patch) | |
| tree | 14b6ae25300dc08c9ca5ff86ad88a78910df7b92 /toplevel | |
| parent | 4f39e160d05b0e5501a909b3041589303651670b (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 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 6 |
2 files changed, 4 insertions, 4 deletions
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" >] |