[skip ci] Update stdpp to 1.10.0

AU-COBRA · Jun 18, 2024 · 96b3ca5 · 96b3ca5
1 parent f663a88
commit 96b3ca5
Show file tree

Hide file tree

Showing 7 changed files with 12 additions and 8 deletions.
diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
@@ -22,7 +22,7 @@ depends: [
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
   "coq-quickchick" {= "dev"}
-  "coq-stdpp" {= "1.9.0"}
+  "coq-stdpp" {= "1.10.0"}
 ]
 build: [
   [make]

diff --git a/coq-concert.opam b/coq-concert.opam
@@ -26,7 +26,7 @@ depends: [
   "coq-metacoq-erasure" {>= "1.3.1" & < "1.4~"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
-  "coq-stdpp" {= "1.9.0"}
+  "coq-stdpp" {>= "1.9.0" & < "1.11~"}
 ]
 
 pin-depends: [

diff --git a/embedding/extraction/PreludeExt.v b/embedding/extraction/PreludeExt.v
@@ -144,12 +144,12 @@ Next Obligation.
   intros a b. destruct a,b; simpl.
   - destruct (n =? n0)%nat eqn:Heq.
     * constructor. now rewrite Nat.eqb_eq in *.
-    * constructor. now rewrite NPeano.Nat.eqb_neq in *.
+    * constructor. now rewrite Nat.eqb_neq in *.
   - now constructor.
   - now constructor.
   - destruct (n =? n0)%nat eqn:Heq.
     * constructor. now rewrite Nat.eqb_eq in *.
-    * constructor. now rewrite NPeano.Nat.eqb_neq in *.
+    * constructor. now rewrite Nat.eqb_neq in *.
 Qed.
 Next Obligation.
   intros ??. unfold base.Decision.

diff --git a/examples/crowdfunding/ExecFrameworkIntegration.v b/examples/crowdfunding/ExecFrameworkIntegration.v
@@ -35,7 +35,7 @@ Definition global_to_tc := compose trans_minductive_entry trans_global_dec.
 Global Program Instance CB : ChainBase :=
   build_chain_base nat Nat.eqb _ _ _ _ Nat.odd. (* Odd addresses are addresses of contracts :) *)
 Next Obligation.
-  eapply NPeano.Nat.eqb_spec.
+  eapply Nat.eqb_spec.
 Defined.
 
 Definition to_chain (sc : SimpleChain_coq) : Chain :=

diff --git a/execution/theories/BuildUtils.v b/execution/theories/BuildUtils.v
@@ -604,7 +604,7 @@ Proof.
     split; eauto.
     do 3 try split; only 9: apply env_eq; eauto; cbn; try lia.
     + now apply finalized_heigh_chain_height.
-    + apply NPeano.Nat.sub_0_le in slot_hit.
+    + apply Nat.sub_0_le in slot_hit.
       rewrite_environment_equiv. cbn. lia.
   - specialize (forward_time_exact bstate reward creator slot) as
       (bstate' & header & reach' & header_valid & slot_hit' & queue' & env_eq); eauto.

diff --git a/execution/theories/Containers.v b/execution/theories/Containers.v
@@ -135,10 +135,11 @@ Module FMap.
       Permutation (keys (add k v' m)) (keys m).
     Proof.
       revert k.
+      (* Search (stdpp.base.lookup _ _ = _ -> Permutation _ _). *)
       induction m using fin_maps.map_ind; intros k find_some.
       + rewrite find_empty in find_some.
         congruence.
-      + destruct (stdpp.base.decide (k = i)) as [->|].
+      + destruct (EqDecision0 k i) as [->|].
         * rewrite fin_maps.insert_insert.
           unfold keys.
           rewrite 2!fin_maps.map_to_list_insert by auto.
@@ -154,6 +155,7 @@ Module FMap.
           now rewrite IHm.
     Qed.
 
+
     Lemma ind (P : FMap K V -> Prop) :
       P empty ->
       (forall k v m, find k m = None -> P m -> P (add k v m)) ->
@@ -193,7 +195,7 @@ Module FMap.
       - rewrite elements_empty, find_empty.
         split; easy.
       - rewrite elements_add by auto.
-        destruct (stdpp.base.decide (k = k0)) as [->|?].
+        destruct (EqDecision0 k k0) as [->|?].
         + rewrite find_add.
           cbn.
           split; intros.

diff --git a/execution/theories/Serializable.v b/execution/theories/Serializable.v
@@ -470,6 +470,8 @@ Section Countable.
            (t : SerializedType) : countable.Countable (interp_type t).
   Proof. induction t; typeclasses eauto. Defined.
 
+  Import (hints) stdpp.base.
+
   Global Instance SerializedValue_EqDecision : stdpp.base.EqDecision SerializedValue.
   Proof.
     intros x y.