Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.

Fixes #14092: Print Grammar ltac2 should exist.

1 files changed, 6 insertions, 0 deletions

diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 6be5ba80d5..7af530ab0f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -50,6 +50,12 @@ let q_pose = Pcoq.Entry.create "q_pose"
 let q_assert = Pcoq.Entry.create "q_assert"
 end
 
+let () =
+  let entries = [
+    Pcoq.AnyEntry Pltac.ltac2_expr;
+  ] in
+  Pcoq.register_grammars_by_name "ltac2" entries
+
 (** Tactic definition *)
 
 type tacdef = {