The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Hi all

Say I have some goal of the form Hyp1 -> Hyp2 -> Hyp3 -> L /\ R and I split and then prove L. Now I have Hyp1-3 above the bar, is there any simple way to add L to the current context?

More generally, if I have several sub-goals g_1, g_2 ... g_n, how can I add a g_i to the context once I prove it?

I know this is being slightly troublesome, and normally I would not bother, only. I'm trying to write some material intended for freshmen and hence can't expose too much of Coq's inner workings to them.

Warm regards
Chris