The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Feb 01, 2007 at 08:46:14AM +0100, Pierre Casteran wrote:

> On the specific point of instantiation propagation :

> Keiko Nakata wrote:

>>- (major) Instantiations may not propagate into other subgoals. 

>> Goal exists x:nat, exists y : nat, y*y = x /\ x = 9.
>> eapply ex_intro.
>> exists 3.
>> split.
>> Focus 2.
>> apply refl_equal.

>> At this point, I get a subgoal containing a non-instantiated
>> variable, which must have been instantiated by the last command
>> "apply refl_equal.".  This is quite unhelpful.

> I tried your example (with a very slight change : Focus was removed
> in order to display all subgoals) and after the tactic call "eapply
> refl_equal" Coq instantiated the existential variable in the first
> subgoal.

That very slight change makes the difference in Coq 8.0pl3. It is a
_bug_ that when one does the focus, it stops instantiation
propagation. Try it with the focus, you'll see. It works fine with "2:
apply refl_equal." indeed.

It seems to be corrected in svn trunk as of 10/1/2007.

Is it also being corrected for 8.0pl4?

-- 
Lionel