base.v 204 Bytes
Newer Older
1 2
From mathcomp.ssreflect Require Export ssreflect.
From prelude Require Export prelude.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Global Set Bullet Behavior "Strict Subproofs".
4 5
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.