• Robbert Krebbers's avatar
    Extend specialization patterns. · 87a8a19c
    Robbert Krebbers authored
    - Support for a `//` modifier to close the goal using `done`.
    - Support for framing in the `[#]` specialization pattern for
      persistent premises, i.e. `[# $H1 $H2]`
    - Add new "auto framing patterns" `[$]`, `[# $]` and `>[$]` that
      will try to solve the premise by framing. Hypothesis that are
      not framed are carried over to the next goal.
    87a8a19c
tactics.v 65.7 KB