aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/printers.mllib2
-rw-r--r--grammar/grammar.mllib2
-rw-r--r--parsing/compat.ml42
-rw-r--r--parsing/tok.mli1
4 files changed, 4 insertions, 3 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 21868203f..39e4b1cdb 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -19,6 +19,7 @@ Pp_control
Loc
CList
CString
+Tok
Compat
Flags
Control
@@ -153,7 +154,6 @@ Library
States
Genprint
-Tok
Lexer
Ppextend
Pputils
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 4432f4306..fc7cb392b 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -49,8 +49,8 @@ Stdarg
Constrarg
Constrexpr_ops
-Compat
Tok
+Compat
Lexer
Entry
Pcoq
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 0e416fe32..c482c694e 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -276,7 +276,7 @@ ELSE
module Gramext = G
let stoken tok = match tok with
| Tok.KEYWORD s -> Gramext.Skeyword s
- | tok -> Gramext.Stoken ((=) tok, G.Token.to_string tok)
+ | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok)
END
IFDEF CAMLP5_6_00 THEN
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 416ce468e..54b747952 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -20,6 +20,7 @@ type t =
| BULLET of string
| EOI
+val equal : t -> t -> bool
val extract_string : t -> string
val to_string : t -> string
(* Needed to fit Camlp4 signature *)