coq-club AT inria.fr
Subject: The Coq mailing list
List archive
RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect
Chronological Thread
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect
- Date: Mon, 30 May 2016 16:05:20 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
- Ironport-phdr: 9a23:mq7r8h8zVa6om/9uRHKM819IXTAuvvDOBiVQ1KB91OscTK2v8tzYMVDF4r011RmSDdSdtqkP2rCempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lS8iP1I/mjaibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0vcVHSODxe7kyZb1eFjUvdW4vroW/vh7aCACL+3E0U2MMkxMODRKTvz/gWZKk+BD9u+Vhwi6CeYXTTLs0UDmmpe8/TR7jiC4KM3gi92zYltZ3lIpapg6so1p0xIuCM9LdD+Z3Yq6IJYBSfmFGRMsEDyE=
Dear Jonathan, Adam,
thanks for the hint! It is much less mysterious now.
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
- [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Soegtrop, Michael, 05/30/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Adam Chlipala, 05/30/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Jonathan Leivent, 05/30/2016
- RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Soegtrop, Michael, 05/30/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Tej Chajed, 05/30/2016
- RE: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Soegtrop, Michael, 05/31/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Dominique Larchey-Wendling, 05/31/2016
- Re: [Coq-Club] Elim of existential hypothesis => Error: Cannot find the elimination combinator ex_rect, Arnaud Spiwack, 05/31/2016
Archive powered by MHonArc 2.6.18.