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