From 975e7cd2ad032668c7df690c9bdaa8cdbb196569 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 15 Sep 2016 16:09:17 +0200
Subject: Moving Ltac-specific generic arguments to their own file in the ltac/
 folder.

---
 grammar/tacextend.mlp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index a1b3f4f25..175853d50 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -61,7 +61,7 @@ let rec mlexpr_of_symbol = function
   <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
 | Uentryl (e, l) ->
   assert (e = "tactic");
-  let arg = get_argt <:expr< Constrarg.wit_tactic >> in
+  let arg = get_argt <:expr< Tacarg.wit_tactic >> in
   <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
 
 let make_prod_item = function
-- 
cgit v1.2.3