The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

Hi all,

On 17/04/2020 20:57, Christian Doczkal wrote:
> I guess the main difference is that is saves a "destruct" whenever
> eliminating an exisist2-hypothesis and a "split" whenever proving one.

This looks like a valid point for `ex2`! Indeed, I sometimes find those
long 'destruct chains' a bit annoying, e.g:


  pose proof my_lemma _ H as (x&L1&L2&L3).


(Of course, I know that you can write an ltac that does this destructing
for you, and I sometimes use this kind of ltac.)

Having n-ary conjunctions is also a nice alternative.

* * * *

I had a quick look into the git history of Coq. It was first committed
quite a while ago, in December 1997, just after the redesign of Coq's
kernel by Jean-Christophe Filliâtre. [1] However, I think it's likely
that `ex2` is even much older, predating the old SVN repo.


[1]: Commit 2b62054dcccae08fdb5b61145e4b84d746e6faf1 (imported from SVN)

Attachment: signature.asc
Description: OpenPGP digital signature