diff options
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" >] |