From b5de86be330f6c878b8f12173d46a4c250fac755 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Mar 2016 18:42:07 +0200
Subject: Moving the code handling tactic notations to Tacentries.

---
 grammar/argextend.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index f9f3ee988e..adfbd8cfde 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -140,7 +140,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
      <:str_item< do {
       Pptactic.declare_extra_genarg_pprule
         $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$;
-      Egramcoq.create_ltac_quotation $se$
+      Tacentries.create_ltac_quotation $se$
         (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v))
         ($lid:s$, None)
       } >> ]
-- 
cgit v1.2.3