base.v 233 Bytes
Newer Older
1
From mathcomp Require Export ssreflect.
2
From iris.prelude Require Export prelude.
3
Set Default Proof Using "Type*".
4
Global Set Bullet Behavior "Strict Subproofs".
5
Global Open Scope general_if_scope.
6
Ltac done := prelude.tactics.done.