From 2cdebfea6858a10c9f9750415d425b445cfbda24 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Thu, 14 Nov 2024 10:56:19 +0100 Subject: [PATCH] compat for Coq 8.18 is easy --- bedrock2/src/bedrock2Examples/metric_LAN9250.v | 6 +++--- bedrock2/src/bedrock2Examples/metric_lightbulb.v | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/metric_LAN9250.v b/bedrock2/src/bedrock2Examples/metric_LAN9250.v index 4f214fc41..85a79c694 100644 --- a/bedrock2/src/bedrock2Examples/metric_LAN9250.v +++ b/bedrock2/src/bedrock2Examples/metric_LAN9250.v @@ -250,7 +250,7 @@ Section WithParameters. progress cbv beta delta [x] in * end; cbn -[Z.add Z.mul Z.of_nat] in *; - rewrite ?length_app, ?List.length_cons, ?List.length_nil in *; + rewrite ?List.app_length, ?List.length_cons, ?List.length_nil in *; flatten_MetricLog; repeat unfold_MetricLog; repeat simpl_MetricLog; try blia. Ltac metrics := solve [metrics']. @@ -916,8 +916,8 @@ Section WithParameters. fnspec! "lan9250_tx" p l / bs ~> err, { requires t m mc := m =*> bytes p bs ∧ l = length bs :> Z ∧ l mod 4 = 0 :> Z; ensures T M MC := M = m ∧ ∃ t', T = t' ++ t ∧ only_mmio_satisfying (fun h => - ((0 <> err ∧ (any+++spi_timeout) h) ∨ (0 = err ∧ lan9250_send bs h ∧ - MC - mc <= (50+6*l)*mc_spi_xchg_const + (length h)*mc_spi_mul))%metricsH) t' + ((0 <> err ∧ (any+++spi_timeout) h) ∨ (0 = err ∧ lan9250_send bs h ∧ + MC - mc <= (50+6*l)*mc_spi_xchg_const + (length h)*mc_spi_mul))%metricsH) t' }. Lemma lan9250_tx_ok' : program_logic_goal_for_function! lan9250_tx. diff --git a/bedrock2/src/bedrock2Examples/metric_lightbulb.v b/bedrock2/src/bedrock2Examples/metric_lightbulb.v index 3a7b83ac3..f4c9fe658 100644 --- a/bedrock2/src/bedrock2Examples/metric_lightbulb.v +++ b/bedrock2/src/bedrock2Examples/metric_lightbulb.v @@ -204,7 +204,7 @@ Section WithParameters. progress cbv beta delta [x] in * end; cbn -[Z.add Z.mul Z.of_nat] in *; - rewrite ?List.length_app, ?List.length_cons, ?List.length_nil, ?List.length_firstn, ?LittleEndianList.length_le_split in *; + rewrite ?List.app_length, ?List.length_cons, ?List.length_nil, ?List.firstn_length, ?LittleEndianList.length_le_split in *; flatten_MetricLog; repeat unfold_MetricLog; repeat simpl_MetricLog; try blia. Local Hint Mode map.map - - : typeclass_instances. (* COQBUG https://github.com/coq/coq/issues/14707 *)