base.v 194 Bytes
Newer Older
1
From mathcomp Require Export ssreflect.
2
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.