diff options
| author | Pierre-Marie Pédrot | 2016-05-11 10:30:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-11 11:23:11 +0200 |
| commit | 17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c (patch) | |
| tree | bf8244fee91d6d0784a59c3dcdfe4e72507e1674 /ltac | |
| parent | f2983cec3544473b18ebc4d4e3a20b941decd196 (diff) | |
Moving the grammar summary to Pcoq.
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 *) |