deprecated.v 174 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5
From iris.algebra Require Import ofe.

(* Old notation for backwards compatibility. *)

(* Deprecated 2016-11-22. Use ofeT instead. *)
6
Notation cofeT := ofeT (only parsing).