Adapt to coq/coq#18880 (#415)

mit-plv · Apr 11, 2024 · 15b0b22 · 15b0b22
1 parent 383e9dc
commit 15b0b22
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/bedrock2/src/bedrock2Examples/BenchCancel256.v b/bedrock2/src/bedrock2Examples/BenchCancel256.v
@@ -5,9 +5,10 @@ Local Open Scope list_scope. Local Open Scope sep_scope.
 (* https://arxiv.org/pdf/1305.6543.pdf figure 4 *)
 (* https://github.com/gmalecha/bedrock-mirror-shard/blob/ea7e5ad56a1d6392468b6823e0457dd44524bca7/benchmarks/MicroBenchCancel.v#L45-L65 *)
 
-Context
+Parameters
   (mem : map.map nat nat) (mem_ok : map.ok mem)
   (ptsto : nat -> nat -> mem -> Prop).
+Existing Instance mem_ok.
 
 Fixpoint chain (ls : list nat) : list (mem -> Prop) :=
   match ls with