From b305aaab36494c2157d7a77444befc552b95e9bd Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 20 Dec 2018 13:56:22 +0100
Subject: [PATCH] Naming

---
 theories/logic/spec_ra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index cfd8a29..ffe5550 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -7,8 +7,8 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang lifting.
 Import uPred.
 
-Definition logrelN := nroot .@ "logrel".
-Definition specN := logrelN .@ "spec".
+Definition relocN := nroot .@ "reloc".
+Definition specN := relocN .@ "spec".
 
 (** The CMRA for the heap of the specification. *)
 Definition tpoolUR : ucmraT := gmapUR nat (exclR exprC).
-- 
GitLab