From 17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 10:30:49 +0200
Subject: Moving the grammar summary to Pcoq.

---
 ltac/tacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index f829ae4f57..5c1e7c0330 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) =
 let tactic_grammar =
   create_grammar_command "TacticGrammar" add_tactic_entry
 
-let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn)
+let extend_tactic_grammar kn ml ntn = extend_grammar_command tactic_grammar (kn, ml, ntn)
 
 (**********************************************************************)
 (* Tactic Notation                                                    *)
-- 
cgit v1.2.3