coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Why does omega try to instantiate evars (sometimes)

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Why does omega try to instantiate evars (sometimes)
Date: Thu, 22 Sep 2016 14:18:33 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.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 mga07.intel.com
Ironport-phdr: 9a23:GoNdwhIoYVAso9oUqNmcpTZWNBhigK39O0sv0rFitYgULPnxwZ3uMQTl6Ol3ixeRBMOAuqgC07ad7PuocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+kQMiK04/ojKibwN76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtM0rzyMF8fkm7otLVbjwV6U+V71RSjo8eShh78ry8BLHUAGn530GU2xQnAAeUCbf6xSvFKz2vyTmrO1lnGG/PMb2RL0wE3z26qZgSBbljGEcMDM27HvQkuRxir5WpFSqoBkpkN2cW52cKPcrJvCVRtgdX2cUBss=

Dear Frédéric,

I can confirm that the mylia tactic works in 8.5pl2. But it is far from
obvious what your wrapper does and how and why. Would you mind writing a few
lines on this or give some pointers?

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] Why does omega try to instantiate evars (sometimes), Soegtrop, Michael, 09/22/2016
- Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Frédéric Besson, 09/22/2016
  - Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Laurent Thery, 09/22/2016
  - RE: [Coq-Club] Why does omega try to instantiate evars (sometimes), Soegtrop, Michael, 09/22/2016
    - Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Frédéric Besson, 09/22/2016
      - RE: [Coq-Club] Why does omega try to instantiate evars (sometimes), Soegtrop, Michael, 09/22/2016
- Re: [Coq-Club] Why does omega try to instantiate evars (sometimes), Jonathan Leivent, 09/22/2016