From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Mar 2016 16:57:05 +0100
Subject: Removing the special status of generic entries defined by Coq itself.

The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.

After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
---
 plugins/cc/g_congruence.ml4 | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/cc')

diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 5dbc340caa..9a53e2e16a 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -9,6 +9,10 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Cctac
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 
 DECLARE PLUGIN "cc_plugin"
 
-- 
cgit v1.2.3