deprecated.v 543 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
(*
FIXME

Ralf Jung's avatar
Ralf Jung committed
4
From iris.base_logic Require Import primitive.
5
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
6 7 8 9 10 11 12 13 14 15

(* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
Notation "■ φ" := (uPred_pure φ%C%type)
    (at level 20, right associativity, only parsing) : uPred_scope.

(* Deprecated 2016-11-22. Use ⌜x = y⌝ instead. *)
Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) (only parsing) : uPred_scope.

(* Deprecated 2016-11-22. Use ⌜x ⊥ y ⌝ instead. *)
Notation "x ⊥ y" := (uPred_pure (x%C%type ⊥ y%C%type)) (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
*)