The Coq mailing list

[Florian Hatat <florian.hatat AT ens-lyon.fr>]

Marko Malikoviæ wrote :
> 2 subgoals
> 
>   H : P 5 2
>   For_rewriting : 2 = 100
>   ============================
>    P 5 2
> 
> subgoal 2 is:
>  P 6 4
> 
> Unnamed_thm < assumption;rewrite For_rewriting in H.

";" means that the second tactic will be applied to all subgoals (and
only them) generated by the first tactic.

In your example, "assumption" solves the first subgoal: it does not
generate any new subgoal, so "rewrite" is applied to nothing.

One step before in your script, you could write:

split; [assumption | rewrite For_rewriting in H].

which means that "split" generates two subgoals, "assumption" is applied
to the first one, "rewrite" to the second one.

-- 
Florian,
http://openweb.eu.org/
http://www.linux-france.org/

Attachment: signature.asc
Description: OpenPGP digital signature