Skip to content

Make `iAssumption` work on `⊢ ...` premises in the Coq context.

Robbert Krebbers requested to merge robbert/iAssumption into master

Moreover, fix errors of iAssumption, iExact, and friends.

  • The error messages were wrong: the goal needs to be absorbing, not the hypothesis.
  • The wrong failure number was used in iAssumption, which caused the error not to be propagated properly.

Merge request reports