From c5c0d37369613aafd074e4beeba5d3d300a07909 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Oct 2014 19:54:36 -0400
Subject: [PATCH] Allow memory refinements to behave like simple renaming.

Memory refinements now carry a boolean parameter that has the following
meaning:

[false] : Behave like a simple renaming of memories that merely allows to
          permute object identifiers. It does not allow to refine memories
          into a more defined version.
[true]  : Behave like before. Objects can be injected, and memory contents can
          be refined into a more defined variant.

We make refinements parametric in these two variant to avoid code duplication,
and because the [false] variant is a special case of the [true] variant.

For completeness of the executable semantics, we now use the [false] variant.
---
 theories/base.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 2ff07170..3a72ad12 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -744,6 +744,8 @@ Class FreshSpec A C `{ElemOf A C,
 (** * Booleans *)
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
+Hint Unfold Is_true.
+Hint Resolve orb_prop_intro andb_prop_intro.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).
 Infix "&&*" := (zip_with (&&)) (at level 40).
-- 
GitLab