The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Tue, Mar 12, 2013 at 12:40:49PM +0100, Arnaud Spiwack wrote:
> Goal True /\ True.
> Proof.
> split.
> - abstract (exact I)
> - exact I
> Defined.

Assuming you have

  Lemma stuck {P Q} (h : P -> Q) (p : P) : Q. Proof. exact (h p). Qed.

The proof term would be one of the following one:

  stuck (fun p => Conj p I) I
  let p := I in Conj p I

The first option has an extra cost, since P is repeated twice and Q
once.  The latter is cheap, but can be used only for transparent side
effects (like elimination principles).

The abstracted term I is there, so the concerns of Adam may be relevant
if you start comparing proofs.  And yes, you are right, these changes
are non local.  I perform them at the very end, when the proof status is
transformed into a proof term by applying the substitution to the
initial evar.

Cheers
-- 
Enrico Tassi