The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Ian,

  actually, in the particular case you were considering the proofs were definitionally equal

so just defining the corresponding obligations with Defined instead of Qed suffices to be

able to apply Same later.

  Program.Tactics also has a few tactics for dealing with proof irrelevance you can get

inspiration from.

-- Matthieu

Le 1 mars 10 à 16:37, Adam Koprowski a écrit :

Thanks, but how do I actually tell coq to apply it to the right places?

I'd rather not have to write out
   assert (EnlargeTransitiveCommuteRelation2_obligation_4 ... =
           EnlargeTransitiveCommuteRelation2_obligation_1 ...).
       apply proof_irrelevance.
etc. if I can get away without it.

  You should be able to write custom Ltac macros that will do that for you. 

  Best,

  Adam

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