diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 86c6f14158..a043a802ab 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4953,7 +4953,6 @@ sig 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 pattern_ident : Id.t Gram.entry val pattern_identref : Id.t located Gram.entry val base_ident : Id.t Gram.entry |