From f759aaf9de94a11aa34a31c869829d60243d273d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 13 Mar 2020 07:17:57 -0400
Subject: [pcoq] Inline the exported Gramlib interface instead of exposing it
 as G

---
 user-contrib/Ltac2/tac2entries.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'user-contrib/Ltac2/tac2entries.mli')

diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 1efac697aa..edad118dc9 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
 (** {5 Notations} *)
 
 type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule
 
-- 
cgit v1.2.3