X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FPreamble.v;h=6abdd71f4d112cd81c1bc71d1d8a7b5825afc49a;hp=026d6d1d017981e750fd8049b500e6574099ff81;hb=bcb16a7fa1ff772f12807c4587609fd756b7762e;hpb=112daf37524662d6d2267d3f7e50ff3522683b8f

diff --git a/src/Preamble.v b/src/Preamble.v
index 026d6d1..6abdd71 100644
--- a/src/Preamble.v
+++ b/src/Preamble.v
@@ -91,7 +91,7 @@ Reserved Notation "a '⊢ᴛy'  b : c"              (at level 20, b at level 99,
 Reserved Notation "a '⊢ᴄᴏ'  b : c ∼ d"          (at level 20, b at level 99).
 Reserved Notation "Γ '+'    x : c"              (at level 50, x at level 99).
 Reserved Notation "Γ '++'   x : a ∼ b"          (at level 50, x at level 99).
-Reserved Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃"           (at level 11, φ₂ at level 99, right associativity).
+Reserved Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"               (at level 11, φ₂ at level 99, right associativity).
 
 Reserved Notation "Γ > past : present '⊢ᴇ' succedent"
    (at level 52, past at level 99, present at level 50, succedent at level 50).