From b70cb4e567ff4917aff54f052f666374e6b3651d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 Nov 2017 16:31:46 +0100
Subject: Remove pidentref grammar entry.

Replaced by ident_decl in #688.
---
 API/API.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 8a4a6cc891..730f17e44f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4941,7 +4941,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
-- 
cgit v1.2.3