Missing low-level Ltac2 primitives (Summary)

[jfehrle]

Summarizes the following missing-primitive PRs. Feel free to add additional missing items until this issue is closed (after which we can open another issue, if needed).

#11837 Ltac2 should expose the contents of the cast type
#12601 Low-level Ltac2 binder API is not low-level enough
#12538, sort-of Ltac2 should expose utility types from OCaml (or bundle reimplementations of them)
#11641 (comment) Ltac2: how to change a constr term with a constr term?
#10940 Ltac2 Constr.Unsafe.case type should expose the inductive and the number of parameters
#10095 Get list of constructors of Inductive
#10369 [Ltac2] : Add system functions for writing and reading files and running processes

These correspond to item # 4 here: #12085 (comment)

Even though Ltac2 allows more low-level access, there are a number of low-level primitives that are missing, and thus are show-stoppers for writing automation that needs them. For example, there's no way currently to get the number of constructors of an inductive type, etc, so we can't write automation that's generic over inductive types. And we can't build terms with casts via the low-level API because the cast type is opaque (#11837). And more.