From 15b0b22f42f64efadc3feea6e812c633745cf0ee Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 11 Apr 2024 18:30:12 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18880 (#415) --- bedrock2/src/bedrock2Examples/BenchCancel256.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/bedrock2/src/bedrock2Examples/BenchCancel256.v b/bedrock2/src/bedrock2Examples/BenchCancel256.v index d45c34d21..34515ee15 100644 --- 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