From 595b04193ba65210304f0e2d9f3a766856feecaa Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Feb 2016 00:10:15 +0100
Subject: [PATCH] Most language notation keywords include a colon: now if does
 too.

---
 heap_lang/notation.v | 2 +-
 heap_lang/tests.v    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index f4727ae5f..161f33f18 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -39,7 +39,7 @@ Notation "'rec:' f x := e" := (Rec f x e%L)
   (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
 Notation "'rec:' f x := e" := (RecV f x e%L)
   (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
-Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
+Notation "'if:' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
   (at level 200, e1, e2, e3 at level 200) : lang_scope.
 
 (** Derived notions, in order of declaration. The notations for let and seq
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 360cb3630..70ef55fff 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -51,10 +51,10 @@ Section LiftingTests.
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + '1 in
-      if "yp" < "x" then "pred" "x" "yp" else "y".
+      if: "yp" < "x" then "pred" "x" "yp" else "y".
   Definition Pred : val :=
     λ: "x",
-      if "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
+      if: "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
 
   Lemma FindPred_spec n1 n2 E Q :
     (■ (n1 < n2) ∧ Q '(n2 - 1)) ⊑ wp E (FindPred 'n2 'n1) Q.
-- 
GitLab