Vague iRevert error messages
iRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)
iRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)