Jason Gross

### Is your feature request related to a problem? I am trying to debug some recursive Ltac2 code I have where (it seems to me) an evar gets instantiated as...

### Description of the problem The doc says: > The complete documentation of canonical structures can be found in [Canonical Structures](https://rocq-prover.org/doc/V8.20.0/refman/language/extensions/canonical.html#canonicalstructures); here only a simple example is given. but the...

Documentation does not specify how to print module definitions

1

### Description of the problem https://rocq-prover.org/doc/V9.1.0/refman/language/core/modules.html#coq:cmd.Print-Module > Command Print Module [qualid](https://rocq-prover.org/doc/V9.1.0/refman/language/core/modules.html#grammar-token-qualid)[](https://rocq-prover.org/doc/V9.1.0/refman/language/core/modules.html#coq:cmd.Print-Module) Prints the module type and (optionally) the body of the module [qualid](https://rocq-prover.org/doc/V9.1.0/refman/language/core/modules.html#grammar-token-qualid). How do I print the body of...

Ltac2 should have a way to print with locally controlled printing flags

2

### Is your feature request related to a problem? I'd like to be able to write something like `Message.of_preterm (preterm:(@Build_some_record _ _ _ _))` and have this print as something...

Ltac2: shortest qualid of name

4

I would like a version of `Env.path` that gives me the shortest qualified name that refers to the given reference.

### Is your feature request related to a problem? I'd like to be able to convert references to message/string ### Proposed solution _No response_ ### Alternative solutions _No response_ ###...

### Is your feature request related to a problem? I would like to be able to convert constructors to message and/or to string ### Proposed solution _No response_ ### Alternative...

[CI] Test that the install directory can be moved

3

This is more-or-less required for the bug minimizer infrastructure to work, and seems to have been broken with the recent renaming. See also https://github.com/coq/coq/pull/20101#issuecomment-2611988918

Registration of user-space Ltac2 conversion / format specifiers

4

### Is your feature request related to a problem? I would like to be able to write concise printf invocations for custom data types. ### Proposed solution Following the principles...

QuickChick is incompatible with standard library Derive plugin (Error: Syntax error: 'for' expected after [constr] (in [command]).)

3

Would it be possible to alter QuickChick so that merely requiring QuickChick does not break Derive in the standard library? (Perhaps by making the syntax factor well with the derive...