base.v 159 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
Require Export mathcomp.ssreflect.ssreflect.
Require Export prelude.prelude.
Global Set Bullet Behavior "Strict Subproofs".
4
Global Open Scope general_if_scope.