From b82f27726f5ae891689e3b958323c2a61d4c154b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:31:08 +0200
Subject: Fixing grammar for "evar" by exporting the test_lpar_id_colon trick
 to EXTEND.

---
 plugins/ltac/extraargs.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/ltac/extraargs.mli')

diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7d4bccfadd..9b41675120 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,6 +67,10 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
-- 
cgit v1.2.3