diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-20 16:31:46 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-20 16:31:46 +0100 |
| commit | b70cb4e567ff4917aff54f052f666374e6b3651d (patch) | |
| tree | 8e88d128861c57039a9cce9cfcb64a99ab4a7143 /parsing/pcoq.mli | |
| parent | 2a857da2a88855a6c9f0fa7e48a8700c1613e0c7 (diff) | |
Remove pidentref grammar entry.
Replaced by ident_decl in #688.
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2f0375419..d17ccb0b4 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -194,7 +194,6 @@ module Prim : val ident : Id.t Gram.entry val name : Name.t located Gram.entry val identref : Id.t located Gram.entry - val pidentref : (Id.t located * (Id.t located list) option) Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : Id.t located Gram.entry |