Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Semantics of simpl

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Semantics of simpl


chronological Thread 
  • From: St�phane Glondu <steph AT glondu.net>
  • To: Kenneth Roe <kendroe AT hotmail.com>
  • Cc: Coq-Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Semantics of simpl
  • Date: Tue, 20 Dec 2011 10:28:51 +0100

Le 20/12/2011 04:30, Kenneth Roe a écrit :
> If instead of executing three separate commands, I combine them as follows:
> 
>     *(eapply simplifyPre; [simplifyState|simpl]).*

Try instead:

 (eapply simplifyPre; [simplifyState|instantiate; simpl])

I'm not sure it will work in your case, but I suspect that it is
"simplifyState" that makes the "AbsExists" appear, but simpl cannot see
it because changes in existential variables (aka "evars", the ones
starting with ?) are not propagated everywhere in a composite tactic. It
works when executing simpl by itself because "." forces evar propagation.


Cheers,

-- 
Stéphane



Archive powered by MhonArc 2.6.16.

Top of Page