Print Ltac2 Type prints available constructors of open types

plugins/ltac2/tac2entries.ml

@@ -1056,7 +1056,19 @@ let print_type ~print_def qid kn =
                  ++ spc() ++ str ": " ++ pr_glbtype name t) ++ str ";"
         in
         hv 2 (str "{ " ++ prlist_with_sep spc pr_field fields ++ str " }")
-      | GTydOpn -> str "[ .. ]"
+      | GTydOpn ->
+        let ctors = KNmap.bindings (Tac2env.find_all_constructors_in_type kn) in
+        if CList.is_empty ctors then str "[ .. ]"
+        else
+          let pr_ctor (ckn, cdata) =
+            let argtys = cdata.Tac2env.cdata_args in
+            hov 0
+              (Tac2print.pr_constructor ckn ++ if CList.is_empty argtys then mt()
+               else spc() ++surround (prlist_with_sep pr_comma (pr_glbtype name) argtys))
+          in
+          hov 0 (str "[ .." ++ spc() ++ str "| "
+                 ++ prlist_with_sep (fun () -> spc() ++ str "| ") pr_ctor ctors
+                   ++ str " ]")
   in
   hov 2 (ty ++ def)
 

plugins/ltac2/tac2env.ml

@@ -89,6 +89,9 @@ let define_constructor kn t =
 
 let interp_constructor kn = KNmap.find kn ltac_state.contents.ltac_constructors
 
+let find_all_constructors_in_type kn =
+  KNmap.filter (fun _ data -> KerName.equal kn data.cdata_type) (!ltac_state).ltac_constructors
+
 let define_projection kn t =
   let state = !ltac_state in
   ltac_state := { state with ltac_projections = KNmap.add kn t state.ltac_projections }

plugins/ltac2/tac2env.mli

@@ -62,6 +62,9 @@ type constructor_data = {
 val define_constructor : ltac_constructor -> constructor_data -> unit
 val interp_constructor : ltac_constructor -> constructor_data
 
+val find_all_constructors_in_type : type_constant -> constructor_data KNmap.t
+(** Useful for printing info about currently defined constructors of open types. *)
+
 (** {5 Toplevel definition of projections} *)
 
 type projection_data = {

test-suite/output/ltac2_printabout.out

@@ -23,3 +23,4 @@ Ltac2 Type 'a ref := { mutable contents : 'a; }
 Ltac2 Type
 ('a, 'b, 'c) trirecord := { cproj : 'c; mutable bproj : 'b; aproj : 'a; }
 Ltac2 Type extensible := [ .. ]
+Ltac2 Type extensible := [ .. | OtherThing (bool) | Thing (string) ]

test-suite/output/ltac2_printabout.v

@@ -66,3 +66,8 @@ Print trirecord.
 Ltac2 Type extensible := [ .. ].
 
 Print extensible.
+
+Ltac2 Type extensible ::= [ Thing (string) ].
+Ltac2 Type extensible ::= [ OtherThing (bool) ].
+
+Print extensible.