Print a sentence with the notation interpretation, scope resolution, and explicit arguments

[darbyhaller]

Hi,

I would like to be able to print a given input sentence with the notation interpreted, all arguments explicit, and the scopes resolved by Coq's internalization process.

For example, after inputting (Add () "Lemma test: forall n:nat, n = n. Proof. assert (H: forall n, n + 0 = n).") and executing it, applying some query command to the sentence assert (H: forall n, n + 0 = n). would return assert (H : forall (n:nat), @eq nat (Nat.add n O) n).
(and nat would instead be Coq.Init.Datatypes.nat, Nat.add would be Coq.Init.Nat.add, etc.)

[ejgallego]

Ack, as discussed on Gitter there are several alternatives; I will prepare a proposal to expose internalization next week, let's see if that's enough for your use case.

[vsiles]

Is there any progress on that front, or can I help in some ways ?

[ejgallego]

#72 should solve this problem to some extent.