coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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: Thu, 24 Jul 2014 16:28:26 +0200
Try this in trunk. It will hopefully explain better than words:
Currently the only way to introduce dependent subgoal is to use the [refine] tactic.
Goal exists n, n=0.
Proof.
refine (ex_intro _ _ _).
Proof.
refine (ex_intro _ _ _).
Currently the only way to introduce dependent subgoal is to use the [refine] tactic.
On 24 July 2014 15:05, Jonathan <jonikelee AT gmail.com> wrote:
On 07/24/2014 05:27 AM, Arnaud Spiwack wrote:
... the new dependent subgoal feature
What is the new dependent subgoal feature?
-- Jonathan
- 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.), Xavier Leroy, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- [Coq-Club] nice evar tactics (was: Re: Prop smuggling (was: Re: Smart case analysis in Coq.)), Jonathan, 07/23/2014
- 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.), 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.), 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.), Xavier Leroy, 07/23/2014
Archive powered by MHonArc 2.6.18.