Commit 1fb71585 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix scopes for if then else to also work with sumbool.

parent 8958d1a5
Require Export mathcomp.ssreflect.ssreflect.
Require Export prelude.prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment