diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |