aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r--parsing/pcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b017fddc7..4565b87a0 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -67,7 +67,7 @@ let weaken_entry x = Gramobj.weaken_entry x
*)
type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
-| Atoken : Tok.t -> ('self, Tok.t) entry_key
+| Atoken : Tok.t -> ('self, string) entry_key
| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key