From d04287bc50ba4b4f1536eb33b930cb2dccaa1280 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 22 Nov 2016 17:19:30 +0100
Subject: [PATCH] make deprecated notation only parsing

---
 algebra/deprecated.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/deprecated.v b/algebra/deprecated.v
index fe84abfd2..d13f5d786 100644
--- 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).
-- 
GitLab