Skip to content

Fix issue #206

Robbert Krebbers requested to merge robbert/issue_206 into master

When performing iDestruct ("H" with ...) as "#..." in the case that:

  • H is in the spatial context, and,
  • The BI is not affine

We cannot use the whole spatial context for both proving the premises of H and the resulting goal. As reported in #206 (closed), trying the above tactic currently gives an anomaly.

This MR issues this issue: Performing the above tactic will now consume the spatial premises.

TODO

This MR contains the following function that should be moved to std++:

Definition TC_to_bool (P : Prop)
  {p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : boo

Given a proposition P that is a type class, it will return true if it can find an instance.

Any suggestions for a better name of this function?

Merge request reports