The Coq mailing list

[Victor Porton <porton AT narod.ru>]

It should be introduced a tactic allowing to write easy (one-line) proofs of the fact that two dependent records (of the same type) are equal whenever all their data fields (not conditions) are equal.

 

Of course, this should work only when "proof irrelevance" axiom is set.

 

03.10.2012, 16:04, "Arnaud Spiwack" <arnaud AT spiwack.net>:

> (cc-ed on Coq-club in case someone interested would not read coqdev, however if you are not following Coq's developpement or at least aren't an active Ltac hacker, this mail probably won't interest you)
>  
> The branch new-tacticals (which was the main subject of the last "GT", see here: http://coq.inria.fr/cocorico/CoqDevelopment/CRGTCoq20120920 ) is now available publicly on github ( https://github.com/aspiwack/coq ). And I'm certainly accepting pull requests (it will be rebased  frequently on the trunk from the official github coq mirror) as I've reached a point where my own perspective is not enough.