Stdpp 1.7.0

[swils]

The main thing with supporting std++ 1.7 and Coq 8.15.0 was another typeclass resolution problem. In the 4 refinement goals, it resolves to (@ptr_type_check K (@rank_eq_dec K (@int_coding K (@env_type_env K H))) H) instead of (@ptr_type_check K EqDecision0 H). I think this change is caused by Coq 8.15, but I have trouble figuring out why.

The other two are small renames. These do prevent backwards compatibility.

[robbertkrebbers]

Thanks for this!

With regard to your question, Coq has issues automatically infering the Decision instance for frozen. In a previous PR, you hacked around that using an unfold and auto with typeclass_instances, but that hack backfired now :joy:.

I am not sure why Coq fails to infer that Decision instance for frozen, but in general it's good taste to make such definitions TC opaque and re-declare instances. Here's a patch that does that:

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