Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)
  • Date: Fri, 25 Jul 2014 08:36:34 +0200


Can one transform an existing evar into such a thing?  Or only those introduced by refine?

 I don't have a good method to transform otherwise introduced existential variables into goals at the moment. Either they were introduced by a refine, or you can use the Grab Existential Variables command when no goal is left to turn all the remaining existential variables into goals.




Archive powered by MHonArc 2.6.18.

Top of Page