coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question on assert + specialize in tactic script

From: Rui Baptista <ruibaptista88 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question on assert + specialize in tactic script
Date: Fri, 6 Feb 2015 14:27:41 +0000

You forgot to unfold GetFirstArg in the hypothesis that was asserted.
Without unfolding it, that hypothesis depends on the hypothesis you're
trying to specialize.

Tactic Notation "SpecializeFirstArg" hyp(H) "by" tactic(tac) :=
let H' := fresh "FirstArg" in
(assert(GetFirstArg H) as H' by (unfold GetFirstArg; tac)); unfold
GetFirstArg in H'; specialize (H H') .

[Coq-Club] Question on assert + specialize in tactic script, Soegtrop, Michael, 02/06/2015
- Re: [Coq-Club] Question on assert + specialize in tactic script, Rui Baptista, 02/06/2015
  - RE: [Coq-Club] Question on assert + specialize in tactic script, Soegtrop, Michael, 02/06/2015