The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

CHA Reeseo wrote:
> I have a new (but related) question:
>        P : nat ->  Prop
>        H : {x : nat | P x}
>        ============================
>         {y : nat | P y}
>
> This example is too simple and can be proved by "assumption", but let's
> forget about it.  Here,
>   * "destruct H; eexists; eassumption" succeeds, but
>   * "eexists; destruct H; eassumption" fails
> because of the reason above.  But visually, the results of
>   * "destruct H; eexists" and
>   * "eexists; destruct H"
> look the same, and it's somewhat confusing:
>
>        P : nat ->  Prop
>        x : nat
>        p : P x
>        ============================
>         P ?6
>
> Does Coq have any command or configuration option to enable some kind of
> 'visual indication' on the context?  For example, the following is just a
> naive mock-up:
>
>        P : nat ->  Prop
>        (?6 : nat)
>        x : nat
>        p : P x
>        ============================
>         P ?6
>    

That's an interesting idea.  The command [Show Existentials] will print 
the contexts of all remaining existential variables, which at least 
conveys all the same information, though in a more verbose form.