coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simple question about refine in 8.5

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Simple question about refine in 8.5
Date: Mon, 8 Feb 2016 11:18:50 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f174.google.com
Ironport-phdr: 9a23:J8TyoxTmqeeC9vW0TDQIgCsh6tpsv+yvbD5Q0YIujvd0So/mwa64YxWN2/xhgRfzUJnB7Loc0qyN4/+mAzxLusvJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuJM04T2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1AbSy09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGGO5qFqRRugsywHOiY9/Xuf3sBrh6JWuBasvTRwxofVZMeeM/8oLfCVRs8TWWcUBpUZbCdGGI7pKtJXV+c=

On Sun, Feb 7, 2016 at 2:08 PM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
wrote:
> What changed (and isn't explained by the CHANGES entry) is that refine
> handles let-in differently. In particular, in 8.4, refine was behaving
> as if clearbody was called on let-in variables (as you did with your
> "simple refine" testcase). This is no longer the case in 8.5. As a
> consequence, in 8.5, the variable occurs in other subgoals, contrarily
> to 8.4, and thus it is shelved (as it would have been in 8.4, if it had
> occurred the same way).

OK, thanks for the explanation.
--
Daniel Schepler

[Coq-Club] Simple question about refine in 8.5, Daniel Schepler, 02/07/2016
- Re: [Coq-Club] Simple question about refine in 8.5, Guillaume Melquiond, 02/07/2016
  - Re: [Coq-Club] Simple question about refine in 8.5, Daniel Schepler, 02/08/2016