From 0d39643cb813a8a3d755921e9b216354dac41a38 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 13 Jun 2018 12:08:05 +0200
Subject: [PATCH] fix printing notation when importing heap_lang.lang after
 heap_lang.notation

---
 tests/heap_lang.v              |  7 +++----
 theories/heap_lang/lang.v      | 10 ----------
 theories/heap_lang/notation.v  | 11 +++++++++++
 theories/heap_lang/proofmode.v |  1 +
 4 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 2d3f50470..bcc2e47de 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,8 +1,7 @@
-(** This file is essentially a bunch of testcases. *)
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import adequacy.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import lang adequacy proofmode notation.
+(* Import lang *again*. This used to break notation. *)
+From iris.heap_lang Require Import lang.
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index e4e5dc55a..aea432737 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -529,13 +529,3 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
-
-(** Define some derived forms *)
-Notation Lam x e := (Rec BAnon x e).
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV x e := (RecV BAnon x e).
-Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 3751417fa..340f78407 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -2,6 +2,17 @@ From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang tactics.
 Set Default Proof Using "Type".
 
+(** Define some derived forms. Happens in the same file because the order of
+    this and the following notations being defined is very relevant. *)
+Notation Lam x e := (Rec BAnon x e).
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Notation Seq e1 e2 := (Let BAnon e1 e2).
+Notation LamV x e := (RecV BAnon x e).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
+Notation SeqCtx e2 := (LetCtx BAnon e2).
+Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
+
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 7481a1a6d..7631e8a85 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
+From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
 Import uPred.
 
-- 
GitLab