From 99863a96d89bf5e8134812f853f59c071965e575 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 1 Aug 2017 18:49:19 +0200
Subject: [PATCH] Put the internal namespace definitions of the lifetime logic
in the model.
---
theories/lifetime/lifetime_sig.v | 3 ---
theories/lifetime/model/definitions.v | 4 ++++
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 22f12192..f2dd298f 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -5,9 +5,6 @@ From iris.base_logic.lib Require Import boxes fractional.
Set Default Proof Using "Type".
Definition lftN : namespace := nroot .@ "lft".
-Definition borN : namespace := lftN .@ "bor".
-Definition inhN : namespace := lftN .@ "inh".
-Definition mgmtN : namespace := lftN .@ "mgmt".
Module Type lifetime_sig.
(** CMRAs needed by the lifetime logic *)
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 7ee27388..7f286d7a 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -6,6 +6,10 @@ From lrust.lifetime Require Export lifetime_sig.
Set Default Proof Using "Type".
Import uPred.
+Definition borN : namespace := lftN .@ "bor".
+Definition inhN : namespace := lftN .@ "inh".
+Definition mgmtN : namespace := lftN .@ "mgmt".
+
Definition atomic_lft := positive.
(* HACK : We need to make sure this is not in the top-level context,
so that it does not conflict with the *definition* of [lft] that we
--
GitLab