diff options
Diffstat (limited to 'plugins/ltac/tacentries.ml')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4127d28bae..9910796d9c 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj let inTacticGrammar : tactic_grammar_obj -> obj = declare_object {(default_object "TacticGrammar") with - open_function = open_tactic_notation; + open_function = simple_open open_tactic_notation; load_function = load_tactic_notation; cache_function = cache_tactic_notation; subst_function = subst_tactic_notation; |