-
Ralf Jung authored
introduce notation to provide "pres" existential witnesses by giving the missing proof. (This is a natural candidate for more ltac magic, to solve these obligations automatically... actually, why can't eauto do that?)
7e5b0b6e
introduce notation to provide "pres" existential witnesses by giving the missing proof. (This is a natural candidate for more ltac magic, to solve these obligations automatically... actually, why can't eauto do that?)