Print alias bodies in Print Ltac2

SkySkimmer · Oct 16, 2023 · 94616b4 · 94616b4
1 parent 3c8ab56
commit 94616b4
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 1 deletion.
diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml
@@ -1033,7 +1033,10 @@ let print_tacref ~print_def qid = function
     let data = Tac2env.interp_global kn in
     let info = Option.map fst (Tac2env.get_compiled_global kn) in
     print_constant ~print_def qid data ?info
-  | TacAlias kn -> str "Alias to ..."
+  | TacAlias kn ->
+    let { Tac2env.alias_body = body } = Tac2env.interp_alias kn in
+    str "Notation" ++ spc() ++ pr_qualid qid ++ str " :=" ++ spc()
+    ++ Tac2print.pr_rawexpr_gen E5 ~avoid:Id.Set.empty body
 
 let print_constructor qid kn =
   let cdata = Tac2env.interp_constructor kn in

diff --git a/test-suite/output/ltac2_printabout.out b/test-suite/output/ltac2_printabout.out
@@ -11,3 +11,4 @@ Inr : 'b -> ('a, 'b) either
 Triple : 'c -> 'b -> 'a -> ('a, 'b, 'c) triple
 Not_found : exn
 Out_of_bounds : message option -> exn
+Ltac2 Notation nota := () ()
diff --git a/test-suite/output/ltac2_printabout.v b/test-suite/output/ltac2_printabout.v
@@ -28,3 +28,9 @@ Print Ltac2 Triple.
 
 Print Ltac2 Not_found.
 Print Ltac2 Out_of_bounds.
+
+(* alias *)
+
+Ltac2 Notation nota := () ().
+
+Print nota.