compat for Coq 8.18 is easy

mit-plv · Nov 14, 2024 · 2cdebfe · 2cdebfe
1 parent b6c1c1e
commit 2cdebfe
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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 *)