From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 24 Oct 2016 18:18:33 +0200
Subject: Lets Hints/Instances take an optional pattern

In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
---
 parsing/pcoq.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9e9a7e723..7dc02190e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -379,6 +379,7 @@ module Vernac_ =
     let vernac = gec_vernac "Vernac.vernac"
     let vernac_eoi = eoi_entry vernac
     let rec_definition = gec_vernac "Vernac.rec_definition"
+    let hint_info = gec_vernac "hint_info"
     (* Main vernac entry *)
     let main_entry = Gram.entry_create "vernac"
     let noedit_mode = gec_vernac "noedit_command"
-- 
cgit v1.2.3