base_logic.v 423 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.bi Require Export bi.
2
From iris.base_logic Require Export derived proofmode.
3
Set Default Proof Using "Type".
4

5 6 7
(* The trick of having multiple [uPred] modules, which are all exported in
another [uPred] module is by Jason Gross and described in:
https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
8
Module Import uPred.
9
  Export base_logic.bi.uPred.
10
  Export derived.uPred.
11
  Export bi.bi.
12
End uPred.