The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there any way to destruct a variable in a way that results in the fresh hypotheses being accessible from an evar?  I would like something like the following to work:

  Ltac evar1_aware_destruct_nat n :=

    instantiate (1 := match n with 0 => _ | _ => _ end);

    let n' := fresh "n'" in

    destruct n as [|n'].

  Goal forall n : nat, exists n0, match n with 0 => 0 | S n' => S n' end = n0.

  Proof.

    intros.

    eexists.

    evar1_aware_destruct_nat n; [ reflexivity | ].

    instantiate (1 := n'). (* Error: Instance is not well-typed in the environment of ?589 *)

Thanks,

Jason