The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Exactly what I was looking for. Thanks!

On Fri, May 31, 2013 at 10:29 PM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

Since 8.4 you can use
  destruct <expr> eqn:<naming intro pattern>

http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic65

The previous (< 8.4) syntax was
  destruct <expr> as ... _eqn
or
  destruct <expr> as ... _eqn:<naming intro pattern>

This "eqn:" syntax also work for "remember" and "induction".

On Sat, Jun 1, 2013 at 4:57 AM, Math Prover <mathprover AT gmail.com> wrote:
> Hi!
>
>   This is a minimal test case of a problem I'm running into.
>
>   Often, when I do "destruct [big complicated _expression_]", I would like to
> have a hypothesis of the form:
>
> H: [big complicated _expression_] = value1
>
>   The reason this shows up is that often I destruct _expression_, but then
> later, when I unfold another _expression_, I need access to the initial
> destructed _expression_. Thus, my question: is there a way to do something
> like "destruct expr; but also remember that expr = ... as a hypothesis"
>
> Thanks!