From 36e865119e5bb5fbaed14428fc89ecd4e96fb7be Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Mar 2016 18:27:39 +0100
Subject: Removing the special status of generic arguments defined by Coq
 itself.

This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.
---
 parsing/pcoq.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'parsing/pcoq.mli')

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 625f0370e6..b1353ef8ad 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -160,6 +160,8 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t
+
 val get_entry : gram_universe -> string -> typed_entry
 
 val create_generic_entry : gram_universe -> string ->
-- 
cgit v1.2.3