The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

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?  

  I believe that 'Show Existentials' is what you are looking for: http://coq.inria.fr/refman/Reference-Manual010.html#@command192.

  Adam

-- 
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]