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:

Goal exists n, n=0.
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)