diff options
Diffstat (limited to 'ltac/tacentries.ml')
| -rw-r--r-- | ltac/tacentries.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2d7b7bf137..d05beb3926 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -511,3 +511,15 @@ let print_ltacs () = hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) + +(** Grammar *) + +let () = + let open Metasyntax in + let entries = [ + AnyEntry Pcoq.Tactic.tactic_expr; + AnyEntry Pcoq.Tactic.binder_tactic; + AnyEntry Pcoq.Tactic.simple_tactic; + AnyEntry Pcoq.Tactic.tactic_arg; + ] in + register_grammar "tactic" entries |