It would be nice if inductives stored their types

[JasonGross]

That is, it would be nice to be able to tell the difference between these three types:

Inductive False1 : Type := .
Inductive False2 (x : Type) : Type := .
Inductive False3 : Type -> Type := .
Quote Recursively Definition qFalse1 := False1.
Quote Recursively Definition qFalse2 := False2.
Quote Recursively Definition qFalse3 := False3.
Print qFalse1. (* Ast.PType "Top.False1" [("False1", {| Ast.ctors := [] |})] ... *)
Print qFalse2. (* Ast.PType "Top.False2" [("False2", {| Ast.ctors := [] |})] ... *)
Print qFalse3. (* Ast.PType "Top.False3" [("False3", {| Ast.ctors := [] |})] ... *)

The reason for this is that I'd like to be able to list all of the inductives in a context, for typechecking, so I don't need to special-case the inductive types that I want to have around.

[gmalecha]

Looks like a good wish.

[aa755]

I was hoping to port the paramcoq plugin to template-coq. In order to accomplish that, I would like to extend the wish to include full reification and reflection of inductive definitions. The reification should contain enough information so that we get the same (except names changes to avoid the clash of constructor names) inductive type on reflecting it back.

[gmalecha]

This information is now available, but not really integrated with everything.

[aa755]

Is this information (parameters and indices of (co)inductives) available somewhere while quoting? In my PR, I only made the datatypes and implemented unquoting