Can I print the partial definition of not finished proof in coq?

Question

Is there any command to print the not finished proof with metavariables?

For example,

Lemma a: forall P Q, (P -> Q) -> P -> Q.
intros.
apply X.

in this state of proof, can I print a := X ? by a command?

Answer 1

You can use the Show Proof command. On your example it prints the following.

(fun (P Q : Type) (X : P -> Q) (X0 : P) => X ?Goal)