make deprecated notation only parsing

d04287bc · Ralf Jung · ef3a26d0 · d04287bc
Commit d04287bc authored Nov 22, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

algebra/deprecated.v algebra/deprecated.v +1 -1

No files found.
--- a/algebra/deprecated.v
+++ b/algebra/deprecated.v
@@ -3,4 +3,4 @@ From iris.algebra Require Import ofe.
 (* Old notation for backwards compatibility. *)

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