coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Inferring a trivial dependency out of no dependency

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Inferring a trivial dependency out of no dependency
Date: Wed, 28 Oct 2015 09:00:44 +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 mga01.intel.com
Ironport-phdr: 9a23:a7XVsBxAXWbnhffXCy+O+j09IxM/srCxBDY+r6Qd0e0VIJqq85mqBkHD//Il1AaPBtWGrasYwLOK6OjJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6PyZ3rnLnuoNX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVG679ZuEzSaFSJDUgKWE8osPx/1GXRgyWo3AYT28+kxxSAgGD4gusDbnrtS6v/NF61SaGJ8ruCfgRWD+i5qpvAle8jSYMNzc09CfMjcF/kLhcuDqgoQByx8jfZ4TDZ6k2Rb/UYd5PHTkJZc1WTSEUWo4=

Dear Yannick,

did you try it in 8.5beta2? Unless I miss something, I would say this all
works as you expect in 8.5beta2 (the things you marked as fail don't fail). I
tested it with the daily build from October 12th.

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, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Inferring a trivial dependency out of no dependency, Yannick, 10/27/2015
- Re: [Coq-Club] Inferring a trivial dependency out of no dependency, Fabian Kunze, 10/27/2015
- RE: [Coq-Club] Inferring a trivial dependency out of no dependency, Soegtrop, Michael, 10/28/2015
  - Re: [Coq-Club] Inferring a trivial dependency out of no dependency, Yannick, 10/28/2015