From 1fb156c31bee9bbf609bb672570fa9b10afdbe94 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 19 Feb 2016 11:38:59 +0100
Subject: [PATCH] Fix levels of step-indexd in validN and includedN.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This fix removes superflous white space in pretty printing. For example
✓{S n} x was pretty printed incorrectly as ✓{(S n)} x.
---
 algebra/cmra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 93126eecc..d8495b8a2 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -21,7 +21,7 @@ Infix "⩪" := minus (at level 40) : C_scope.
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
 Notation "✓{ n } x" := (validN n x)
-  (at level 20, n at level 1, format "✓{ n }  x").
+  (at level 20, n at next level, format "✓{ n }  x").
 
 Class Valid (A : Type) := valid : A → Prop.
 Instance: Params (@valid) 2.
@@ -30,7 +30,7 @@ Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x.
 
 Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
 Notation "x ≼{ n } y" := (includedN n x y)
-  (at level 70, format "x  ≼{ n }  y") : C_scope.
+  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
 Instance: Params (@includedN) 4.
 Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
-- 
GitLab