diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index d92f93484a59186b588de4d152913f3210ed9965..d9cbde34a38ea498e4c8086506b085e0a4eab924 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -171,31 +171,31 @@ Inductive typed_ctx_item :
      typed_ctx_item CTX_Fork Γ () Γ ()
   (* Heap *)
   | TPCTX_Alloc Γ τ :
-     typed_ctx_item CTX_Alloc Γ τ Γ (Tref τ)
+     typed_ctx_item CTX_Alloc Γ τ Γ (TRef τ)
   | TP_CTX_Load Γ τ :
-     typed_ctx_item CTX_Load Γ (Tref τ) Γ τ
+     typed_ctx_item CTX_Load Γ (TRef τ) Γ τ
   | TP_CTX_StoreL Γ e2 τ :
-     typed Γ e2 τ → typed_ctx_item (CTX_StoreL e2) Γ (Tref τ) Γ ()
+     typed Γ e2 τ → typed_ctx_item (CTX_StoreL e2) Γ (TRef τ) Γ ()
   | TP_CTX_StoreR Γ e1 τ :
-     typed Γ e1 (Tref τ) →
+     typed Γ e1 (TRef τ) →
      typed_ctx_item (CTX_StoreR e1) Γ τ Γ ()
   | TP_CTX_FAAL Γ e2 :
      Γ ⊢ₜ e2 : TNat →
-     typed_ctx_item (CTX_FAAL e2) Γ (Tref TNat) Γ TNat
+     typed_ctx_item (CTX_FAAL e2) Γ (TRef TNat) Γ TNat
   | TP_CTX_FAAR Γ e1 :
-     Γ ⊢ₜ e1 : Tref TNat →
+     Γ ⊢ₜ e1 : TRef TNat →
      typed_ctx_item (CTX_FAAR e1) Γ TNat Γ TNat
   | TP_CTX_CasL Γ e1 e2 τ :
      EqType τ → UnboxedType τ →
      typed Γ e1 τ → typed Γ e2 τ →
-     typed_ctx_item (CTX_CmpXchgL e1 e2) Γ (Tref τ) Γ (TProd τ TBool)
+     typed_ctx_item (CTX_CmpXchgL e1 e2) Γ (TRef τ) Γ (TProd τ TBool)
   | TP_CTX_CasM Γ e0 e2 τ :
      EqType τ → UnboxedType τ →
-     typed Γ e0 (Tref τ) → typed Γ e2 τ →
+     typed Γ e0 (TRef τ) → typed Γ e2 τ →
      typed_ctx_item (CTX_CmpXchgM e0 e2) Γ τ Γ (TProd τ TBool)
   | TP_CTX_CasR Γ e0 e1 τ :
      EqType τ → UnboxedType τ →
-     typed Γ e0 (Tref τ) → typed Γ e1 τ →
+     typed Γ e0 (TRef τ) → typed Γ e1 τ →
      typed_ctx_item (CTX_CmpXchgR e0 e1) Γ τ Γ (TProd τ TBool)
   (* Polymorphic & recursive types *)
   | TP_CTX_Fold Γ τ :
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 5ced5e1d310ed950e29d7ae3ff6bc196d623e342..02ac49358f632d988e245676df925f051e0b41f2 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -244,7 +244,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_load Δ Γ e e' τ :
-    ({Δ;Γ} ⊨ e ≤log≤ e' : (Tref τ)) -∗
+    ({Δ;Γ} ⊨ e ≤log≤ e' : (TRef τ)) -∗
     {Δ;Γ} ⊨ Load e ≤log≤ Load e' : τ.
   Proof.
     iIntros "IH".
@@ -254,7 +254,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
     {Δ;Γ} ⊨ Store e1 e2 ≤log≤ Store e1' e2' : ().
   Proof.
@@ -266,7 +266,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_FAA Δ Γ e1 e2 e1' e2' :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref TNat) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef TNat) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : TNat) -∗
     {Δ;Γ} ⊨ FAA e1 e2 ≤log≤ FAA e1' e2' : TNat.
   Proof.
@@ -291,7 +291,7 @@ Section fundamental.
   Lemma bin_log_related_CmpXchg Δ Γ e1 e2 e3 e1' e2' e3' τ
     (HEqτ : EqType τ)
     (HUbτ : UnboxedType τ) :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
     ({Δ;Γ} ⊨ e3 ≤log≤ e3' : τ) -∗
     {Δ;Γ} ⊨ CmpXchg e1 e2 e3 ≤log≤ CmpXchg e1' e2' e3' : TProd τ TBool.
@@ -329,7 +329,7 @@ Section fundamental.
 
   Lemma bin_log_related_alloc Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ) -∗
-    {Δ;Γ} ⊨ Alloc e ≤log≤ Alloc e' : Tref τ.
+    {Δ;Γ} ⊨ Alloc e ≤log≤ Alloc e' : TRef τ.
   Proof.
     iIntros "IH".
     intro_clause.
@@ -343,8 +343,8 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_ref_binop Δ Γ e1 e2 e1' e2' τ :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ) -∗
-    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : Tref τ) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
+    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : TRef τ) -∗
     {Δ;Γ} ⊨ BinOp EqOp e1 e2 ≤log≤ BinOp EqOp e1' e2' : TBool.
   Proof.
     iIntros "IH1 IH2".
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 6f78bac27b393188f27ff4d8a7cf40f911d39433..a87c103b4973da8cc159b9774905ca8c7eebdced 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -37,7 +37,7 @@ Section semtypes.
     | TVar x => ctx_lookup x
     | TForall τ' => λne Δ, lrel_forall (λ τ, interp τ' (τ::Δ))
     | TExists τ' => λne Δ, lrel_exists (λ τ, interp τ' (τ::Δ))
-    | Tref τ => λne Δ, lrel_ref (interp τ Δ)
+    | TRef τ => λne Δ, lrel_ref (interp τ Δ)
     end.
   Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; try solve_proper).
   Next Obligation.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index ad16eb35ef984d6540e07842bed071d1c87f9e2d..a21d6196c5bb81b5cdc304c69a64665540e0361c 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -16,7 +16,7 @@ Inductive type :=
   | TVar : var → type
   | TForall : {bind 1 of type} → type
   | TExists : {bind 1 of type} → type
-  | Tref : type → type.
+  | TRef : type → type.
 
 (** Which types support equality testing *)
 Inductive EqType : type → Prop :=
@@ -31,7 +31,7 @@ Inductive UnboxedType : type → Prop :=
   | UnboxedTUnit : UnboxedType TUnit
   | UnboxedTNat : UnboxedType TNat
   | UnboxedTBool : UnboxedType TBool
-  | UnboxedTref Ï„ : UnboxedType (Tref Ï„).
+  | UnboxedTRef Ï„ : UnboxedType (TRef Ï„).
 
 (** Autosubst instances *)
 Instance Ids_type : Ids type. derive. Defined.
@@ -70,7 +70,7 @@ Notation "∀: τ" :=
 Notation "∃: τ" :=
   (TExists Ï„%ty)
   (at level 100, Ï„ at level 200) : FType_scope.
-Notation "'ref' Ï„" := (Tref Ï„%ty) (at level 10, Ï„ at next level, right associativity): FType_scope.
+Notation "'ref' Ï„" := (TRef Ï„%ty) (at level 10, Ï„ at next level, right associativity): FType_scope.
 
 (** * Typing judgements *)
 Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).