From 862759a06cd431441b8e8d88e134ca779fcb5a2d Mon Sep 17 00:00:00 2001
From: Stefan Wils <stefanwils@gmail.com>
Date: Wed, 9 Feb 2022 11:11:44 +0100
Subject: [PATCH 1/3] Port to Coq 8.15 and stdpp 1.7 (not backwards compatible
 due to renames)

---
 memory/memory_map.v             | 2 +-
 memory/pointer_bits.v           | 2 +-
 refinements/operations_refine.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/memory/memory_map.v b/memory/memory_map.v
index b2d42dc..e35d422 100644
--- a/memory/memory_map.v
+++ b/memory/memory_map.v
@@ -266,7 +266,7 @@ Proof.
   destruct (m !!{Γ} (_, addr_ref _ _)) as [w'|] eqn:?; simplify_equality'.
   erewrite cmap_lookup_ref_le
     by eauto using cmap_lookup_ref_le, ref_freeze_le_r; simpl.
-  by rewrite (decide_iff _ _ _ _ (addr_is_obj_freeze _ _)).
+  by rewrite (decide_ext _ _ _ _ (addr_is_obj_freeze _ _)).
 Qed.
 Lemma cmap_lookup_ref_Some Γ Δ m o r w :
   ✓ Γ → ✓{Γ,Δ} m → m !!{Γ} (o,r) = Some w →
diff --git a/memory/pointer_bits.v b/memory/pointer_bits.v
index e6d7f0f..21d78f4 100644
--- a/memory/pointer_bits.v
+++ b/memory/pointer_bits.v
@@ -36,7 +36,7 @@ Implicit Types pbs : list (ptr_bit K).
 #[global] Instance ptr_bit_valid_dec ΓΔ (pb : ptr_bit K) : Decision (✓{ΓΔ} pb).
 Proof.
  refine
-  match Some_dec (type_check ΓΔ (frag_item pb)) with
+  match Some_dec (@type_check _ _ _ (@ptr_type_check K EqDecision0 H) ΓΔ (frag_item pb)) with
   | inleft (τ↾Hτ) => cast_if_and (decide (frozen (frag_item pb)))
      (decide (frag_index pb < bit_size_of (ΓΔ.1) (τ.*)))
   | inright Hτ => right _
diff --git a/refinements/operations_refine.v b/refinements/operations_refine.v
index 3fa307a..7dccca8 100644
--- a/refinements/operations_refine.v
+++ b/refinements/operations_refine.v
@@ -39,7 +39,7 @@ Lemma addr_compare_refine Γ α f m1 m2 c a1 a2 a3 a4 σp :
   a1 ⊑{Γ,α,f@'{m1}↦'{m2}} a2 : σp → a3 ⊑{Γ,α,f@'{m1}↦'{m2}} a4 : σp →
   addr_compare Γ c a1 a3 = addr_compare Γ c a2 a4.
 Proof.
-  intros ? (_&_&Hstrict) Ha1 Ha2; unfold addr_compare; apply bool_decide_iff.
+  intros ? (_&_&Hstrict) Ha1 Ha2; unfold addr_compare; apply bool_decide_ext.
   assert ('{m1} ⊑{Γ,α,f} '{m2}) as HΔ by eauto using addr_refine_memenv_refine.
   destruct (addr_object_offset_refine Γ α f
     '{m1} '{m2} a1 a2 σp) as (r1&?&?&->); auto.

From 48625f8587afc038235a6373dff36b797c6e3b13 Mon Sep 17 00:00:00 2001
From: Stefan Wils <stefanwils@gmail.com>
Date: Wed, 9 Feb 2022 11:13:16 +0100
Subject: [PATCH 2/3] Updated the README file.

---
 README | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README b/README
index 7986c94..6e53622 100644
--- a/README
+++ b/README
@@ -9,7 +9,7 @@ This version is known to compile with:
  - OCaml-Num 1.4.2
  - OCamlbuild 0.14.0
  - GNU C preprocessor 8.3.0
- - stdpp 1.6.0
+ - stdpp 1.7.0
 
 BUILDING INSTRUCTIONS
 ---------------------

From 210ee5a4e70cfe1269d6629a8989a9f096929ef4 Mon Sep 17 00:00:00 2001
From: Stefan Wils <stefanwils@gmail.com>
Date: Wed, 9 Feb 2022 17:05:08 +0100
Subject: [PATCH 3/3] A proper solution for the TC resolution problem with
 frozen (thx Robbert).

---
 memory/pointer_bits.v | 4 ++--
 memory/references.v   | 5 ++++-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/memory/pointer_bits.v b/memory/pointer_bits.v
index 21d78f4..616643a 100644
--- a/memory/pointer_bits.v
+++ b/memory/pointer_bits.v
@@ -36,11 +36,11 @@ Implicit Types pbs : list (ptr_bit K).
 #[global] Instance ptr_bit_valid_dec ΓΔ (pb : ptr_bit K) : Decision (✓{ΓΔ} pb).
 Proof.
  refine
-  match Some_dec (@type_check _ _ _ (@ptr_type_check K EqDecision0 H) ΓΔ (frag_item pb)) with
+  match Some_dec (type_check ΓΔ (frag_item pb)) with
   | inleft (τ↾Hτ) => cast_if_and (decide (frozen (frag_item pb)))
      (decide (frag_index pb < bit_size_of (ΓΔ.1) (τ.*)))
   | inright Hτ => right _
-  end; unfold frozen; auto with typeclass_instances;
+  end;
   destruct ΓΔ; first
   [ simplify_type_equality; econstructor; eauto
   | by destruct 1 as (?&?&?&?); simplify_type_equality ].
diff --git a/memory/references.v b/memory/references.v
index 6deae74..20976da 100644
--- a/memory/references.v
+++ b/memory/references.v
@@ -68,8 +68,11 @@ Inductive ref_typed' `{Env K} (Γ : env K) :
 
 Class Freeze A := freeze: bool → A → A.
 Arguments freeze {_ _} _ !_ /.
+
 Definition frozen `{Freeze A} (x : A) := freeze true x = x.
-Arguments freeze {_ _} _ !_ /.
+#[global] Typeclasses Opaque frozen.
+#[global] Instance frozen_dec `{EqDecision A, Freeze A} (x : A) :
+  Decision (frozen x) := decide (freeze true x = x).
 
 #[global] Instance ref_seg_freeze {K} : Freeze (ref_seg K) := λ β rs,
   match rs with