base_logic.v 719 Bytes
Newer Older
1
From iris.base_logic Require Export derived.
2
Set Default Proof Using "Type".
3

4 5 6
(* 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 *)
7 8 9 10
Module Import uPred.
  Export upred.uPred.
  Export primitive.uPred.
  Export derived.uPred.
11 12 13
End uPred.

(* Hint DB for the logic *)
14
Hint Resolve pure_intro : I.
15 16
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
17
Hint Resolve persistently_mono : I.
18 19
Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
Hint Immediate True_intro False_elim : I.
20
Hint Immediate iff_refl internal_eq_refl' : I.