diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d13ff548c..959c039d3 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -273,8 +273,8 @@ type ('self, _) entry_key = | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key | Aself : ('self, 'self) entry_key | Anext : ('self, 'self) entry_key -| Atactic : int -> ('self, raw_tactic_expr) entry_key | Aentry : (string * string) -> ('self, 'a) entry_key +| Aentryl : (string * string) * int -> ('self, 'a) entry_key val name_of_entry : 'a Gram.entry -> string * string |