coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- 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 14:41:49 +0100
On Fri, Jul 25, 2014 at 12:55 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:
Also, by the way, is it intended that you have to inspect the hypotheses to get your hands on the name of the evar introduced by [refine (let e : T := _ in _)] in the second goal? That is, to get a fresh named evar as a goal, I do something likeLtac new_style_evar e T :=refine (let e' : T := _ in _);[| let e' := match goal with e' := _ |- _ => constr:(e') end inrename e' into e ].You are right that this is a problem. I'm not sure how to solve that. I'll look into it soon.
It might be nice, in general, if binders respected fresh. For example,
Goal True.
Proof.
let H := fresh "E" in
pose (fun H : Set => H).
should give me [fun E : Set => E], not [fun H : Set => H]. I think this would be enough to solve the problem. Should I make a bug report?
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), (continued)
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/25/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/25/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/25/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/25/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/25/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/25/2014
Archive powered by MHonArc 2.6.18.