From 3660c994fc95e29e2202e1929f7e232b0d95f903 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 6 Jun 2018 18:06:26 +0200
Subject: [PATCH] turns out we don't need the hv in any of this

---
 tests/proofmode.v                   |  2 +-
 theories/bi/notation.v              | 10 +++++-----
 theories/program_logic/weakestpre.v | 20 ++++++++++----------
 theories/proofmode/notation.v       |  4 ++--
 4 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index e45215ab4..e2178b33f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -501,7 +501,7 @@ Proof.
   iIntros "?". Show.
 Abort.
 
-(* This is specifically crafted such that not having the `hv` in
+(* This is specifically crafted such that not having the printing box in
    the proofmode notation breaks the output. *)
 Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P ∧ Q)%I
   (format "'TESTNOTATION'  '{{'  P  '|'  '/' Q  '}' '}'") : bi_scope.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 3a7ab4344..31d7168c9 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -51,34 +51,34 @@ Reserved Notation "'<subj>' P" (at level 20, right associativity).
 (** Update modalities *)
 Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
 Reserved Notation "P ==∗ Q"
-  (at level 99, Q at level 200, format "'[hv  ' P  ==∗  '/' Q ']'").
+  (at level 99, Q at level 200, format "'[  ' P  ==∗  '/' Q ']'").
 
 Reserved Notation "|={ E1 , E2 }=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }=>  Q").
 Reserved Notation "P ={ E1 , E2 }=∗ Q"
   (at level 99, E1,E2 at level 50, Q at level 200,
-   format "'[hv  ' P  ={ E1 , E2 }=∗  '/' Q ']'").
+   format "'[  ' P  ={ E1 , E2 }=∗  '/' Q ']'").
 
 Reserved Notation "|={ E }=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }=>  Q").
 Reserved Notation "P ={ E }=∗ Q"
   (at level 99, E at level 50, Q at level 200,
-   format "'[hv  ' P  ={ E }=∗  '/' Q ']'").
+   format "'[  ' P  ={ E }=∗  '/' Q ']'").
 
 Reserved Notation "|={ E1 , E2 }â–·=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }â–·=>  Q").
 Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "'[hv  ' P  ={ E1 , E2 }▷=∗  '/' Q ']'").
+   format "'[  ' P  ={ E1 , E2 }▷=∗  '/' Q ']'").
 Reserved Notation "|={ E }â–·=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }â–·=>  Q").
 Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
-   format "'[hv  ' P  ={ E }▷=∗  '/' Q ']'").
+   format "'[  ' P  ={ E }▷=∗  '/' Q ']'").
 
 (** Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index d9d4d1638..139a5d78b 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -54,35 +54,35 @@ Instance: Params (@wp) 6.
 
 Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'[hv' 'WP'  e  '/' @  s ;  E  {{  Φ  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' @  s ;  E  {{  Φ  } } ']'") : bi_scope.
 Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'[hv' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : bi_scope.
 Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'[hv' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : bi_scope.
 Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'[hv' 'WP'  e  '/' {{  Φ  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : bi_scope.
 Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'[hv' 'WP'  e  '/' ? {{  Φ  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' ? {{  Φ  } } ']'") : bi_scope.
 
 Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[hv' 'WP'  e  '/' @  s ;  E  {{  v ,  Q  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' @  s ;  E  {{  v ,  Q  } } ']'") : bi_scope.
 Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[hv' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : bi_scope.
 Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[hv' 'WP'  e  '/' @  E  ? {{  v ,  Q  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' @  E  ? {{  v ,  Q  } } ']'") : bi_scope.
 Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[hv' 'WP'  e  '/' {{  v ,  Q  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : bi_scope.
 Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[hv' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : bi_scope.
+   format "'[' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : bi_scope.
 
 (* Texan triples *)
 Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 7f273eb8e..33019f9c1 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -10,10 +10,10 @@ Arguments Esnoc {_} _%proof_scope _%string _%I.
 Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
   (at level 1, P at level 200,
-   left associativity, format "Γ H  :  '[hv' P ']' '//'", only printing) : proof_scope.
+   left associativity, format "Γ H  :  '[' P ']' '//'", only printing) : proof_scope.
 Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
   (at level 1, P at level 200,
-   left associativity, format "Γ '_'  :  '[hv' P ']' '//'", only printing) : proof_scope.
+   left associativity, format "Γ '_'  :  '[' P ']' '//'", only printing) : proof_scope.
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Γ Δ _) Q%I)
-- 
GitLab