coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Easy question re: implicit parameters

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Easy question re: implicit parameters
Date: Mon, 18 Sep 2017 09:16:15 +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 mga06.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.0.116
Ironport-phdr: 9a23:jGylZByzgPsuPxDXCy+O+j09IxM/srCxBDY+r6Qd0uMXIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSj45jkLXx77KABdJ+LvG4eUgd79n7S5/ISWaAFVjhK8Z6lzJVO4t1OCmNMRhN4oEaE8xQfTpWMMM8FXzmNhKFbZ10L558yw9ZNntT9Xtv097clYeaT8Y6k8C7dfCWJ1YCgO+MT3uEybHkO07XwGXzBOnw==

Dear Guillaume,

> For sig: Argument scopes are [type_scope type_scope] ...
> For sig2: Argument scopes are [type_scope type_scope type_scope] ...

I guess the difference comes from the fact that we used a different sig2. I
used the sig2 as I defined it (see the Coq snippet in my post), while you
used the standard library version of sig2. Sorry for the confusing choice of
names.

What I complained about is that when I redefine sig exactly as it is in the
standard library, I get different argument scopes.

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

RE: [Coq-Club] Easy question re: implicit parameters, (continued)