From fe36d6253a31a2d168b654bae5ededd8941fdf9d Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Tue, 18 Jun 2024 20:39:51 +0200
Subject: [PATCH 01/10] Disable broken dearg_transform flags

---
 .../counter/extraction/CounterRefTypesMidlang.v   | 10 +++++++++-
 examples/escrow/extraction/EscrowMidlang.v        |  3 ++-
 extraction/tests/NumLiteralTests.v                | 15 +++++++++++++--
 extraction/theories/LiquidityExtract.v            |  3 ++-
 4 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/examples/counter/extraction/CounterRefTypesMidlang.v b/examples/counter/extraction/CounterRefTypesMidlang.v
index 0390042b..21c4ed17 100644
--- a/examples/counter/extraction/CounterRefTypesMidlang.v
+++ b/examples/counter/extraction/CounterRefTypesMidlang.v
@@ -128,10 +128,18 @@ Definition ignored_concert_types :=
          <%% @ContractCallContext %%>;
          <%% @SerializedValue %%>].
 
+(* TODO: tmp, revert once https://github.com/MetaCoq/metacoq/pull/1030 is resolved *)
+From MetaCoq.Erasure.Typed Require Import Optimize.
+Definition extract_within_coq : extract_template_env_params :=
+  {| template_transforms := [];
+     check_wf_env_func Σ := Ok (assume_env_wellformed Σ);
+     pcuic_args :=
+       {| optimize_prop_discr := true;
+          extract_transforms := [dearg_transform (fun _ => None) true false true true true] |} |}.
 
 Definition counter_extract :=
     Eval vm_compute in
-    extract_template_env_within_coq
+    extract_template_env extract_within_coq
       counter_env
       (KernameSet.singleton counter_name)
       (fun kn => List.existsb (eq_kername kn)
diff --git a/examples/escrow/extraction/EscrowMidlang.v b/examples/escrow/extraction/EscrowMidlang.v
index 3e639e59..cdf02b75 100644
--- a/examples/escrow/extraction/EscrowMidlang.v
+++ b/examples/escrow/extraction/EscrowMidlang.v
@@ -62,7 +62,8 @@ Definition extract_params :=
      template_transforms := [template_inline should_inline];
      pcuic_args :=
        {| optimize_prop_discr := true;
-          extract_transforms := [Optimize.dearg_transform (fun _ => None) true true true true true] |} |}.
+          (* TODO: tmp, revert once https://github.com/MetaCoq/metacoq/pull/1030 is resolved *)
+          extract_transforms := [Optimize.dearg_transform (fun _ => None) true false true true true] |} |}.
 
 Axiom extraction_chain_base : ChainBase.
 #[local]
diff --git a/extraction/tests/NumLiteralTests.v b/extraction/tests/NumLiteralTests.v
index 103974da..342d3c8d 100644
--- a/extraction/tests/NumLiteralTests.v
+++ b/extraction/tests/NumLiteralTests.v
@@ -50,12 +50,23 @@ Open Scope monad_scope.
 
 Definition result_err_bytestring A := result A bytestring.String.t.
 
+(* TODO: tmp, revert once https://github.com/MetaCoq/metacoq/pull/1030 is resolved *)
+Import List.
+Import ListNotations.
+From MetaCoq.Erasure.Typed Require Import Optimize.
+Definition extract_within_coq : extract_template_env_params :=
+  {| template_transforms := [];
+     check_wf_env_func Σ := Ok (assume_env_wellformed Σ);
+     pcuic_args :=
+       {| optimize_prop_discr := true;
+          extract_transforms := [dearg_transform (fun _ => None) true false true true true] |} |}.
+
 Definition extract_ (p : program) : result_err_bytestring _ :=
   entry <- match snd p with
            | tConst kn _ => ret kn
            | _ => Err (s_to_bs "Expected program to be a tConst")
            end;;
-  extract_template_env_within_coq
+  extract_template_env extract_within_coq
          (fst p)
          (Kernames.KernameSet.singleton entry)
          (fun k => false).
@@ -66,7 +77,7 @@ Definition extract_body {A} (def : A) : TemplateMonad _ :=
            | tConst kn _ => ret kn
            | _ => tmFail (s_to_bs "Expected program to be a tConst")
           end ;;
-  res <- tmEval Common.lazy (extract_template_env_within_coq
+  res <- tmEval Common.lazy (extract_template_env extract_within_coq
                (fst p)
                (Kernames.KernameSet.singleton entry)
                (fun k => false));;
diff --git a/extraction/theories/LiquidityExtract.v b/extraction/theories/LiquidityExtract.v
index c40f9658..689906ba 100644
--- a/extraction/theories/LiquidityExtract.v
+++ b/extraction/theories/LiquidityExtract.v
@@ -83,7 +83,8 @@ Definition extract_liquidity_within_coq (to_inline : kername -> bool)
           extract_transforms :=
             (* TODO: a 'false' second-last arg disables fully
                expanded environments - only for boardroomvoting *)
-            [dearg_transform overridden_masks true true true true true]
+            (* TODO: tmp, revert once https://github.com/MetaCoq/metacoq/pull/1030 is resolved *)
+            [dearg_transform overridden_masks true false true true true]
        |}
   |}.
 

From 9d19164d5ec87d9930036c0be21663d9eeec9b00 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Tue, 18 Jun 2024 14:08:44 +0200
Subject: [PATCH 02/10] Port ConCert core to MetaCoq 1.3.1

---
 embedding/theories/pcuic/PCUICCorrectnessAux.v | 12 ++++++------
 embedding/theories/pcuic/PCUICTranslate.v      |  8 ++++----
 extraction/theories/CameLIGOPretty.v           |  2 ++
 extraction/theories/LiquidityPretty.v          |  2 ++
 4 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/embedding/theories/pcuic/PCUICCorrectnessAux.v b/embedding/theories/pcuic/PCUICCorrectnessAux.v
index 5c6c0336..a5673a7d 100644
--- a/embedding/theories/pcuic/PCUICCorrectnessAux.v
+++ b/embedding/theories/pcuic/PCUICCorrectnessAux.v
@@ -240,9 +240,9 @@ Lemma type_value_term_value Σ ty :
   PcbvCurr.value Σ (type_to_term ty).
 Proof.
   intros Hc Hty. induction Hty.
-  + simpl. constructor. apply tInd_atom.
-  + simpl. now constructor.
+  + simpl. constructor. constructor. apply tInd_atom.
   + simpl. now constructor.
+  + simpl. constructor. now constructor.
   + simpl in *. propify. destruct_hyps.
     erewrite decompose_inductive_mkApps by eauto.
     rewrite <- mkApps_unfold.
@@ -250,7 +250,7 @@ Proof.
     * apply tInd_value_head.
     * apply All_app_inv; eauto.
       eapply decompose_inductive_value with (t1 := ty1); eauto.
-  + constructor; eauto.
+  + do 2 constructor; eauto.
 Qed.
 
 #[export] Hint Constructors ty_val : hints.
@@ -369,9 +369,9 @@ Proof.
     inversion Hok; subst.
     eapply Wcbv_value_vars_to_apps; eauto.
     eapply All_impl_inner; eauto.
-  + destruct cm. constructor; auto.
-    simpl. now constructor.
-  + simpl in *. constructor; auto.
+  + destruct cm. do 2 constructor; auto.
+    simpl. now do 2 constructor.
+  + simpl in *. do 2 constructor; auto.
   + simpl in *.
     inversion Hok; subst. now eapply type_value_term_value.
 Qed.
diff --git a/embedding/theories/pcuic/PCUICTranslate.v b/embedding/theories/pcuic/PCUICTranslate.v
index 6634aff0..a4565a5a 100644
--- a/embedding/theories/pcuic/PCUICTranslate.v
+++ b/embedding/theories/pcuic/PCUICTranslate.v
@@ -35,7 +35,7 @@ Reserved Notation "T⟦ ty ⟧ " (at level 5).
 Fixpoint type_to_term (ty : type) : term :=
   match ty with
   | tyInd i => tInd (mkInd (kername_of_string i) 0) []
-  | tyForall nm ty => tProd (aRelevant (nNamed (TCString.of_string nm))) (tSort Universe.type0) T⟦ty⟧
+  | tyForall nm ty => tProd (aRelevant (nNamed (TCString.of_string nm))) (tSort Sort.type0) T⟦ty⟧
   | tyVar nm => tVar (TCString.of_string nm)
   | tyApp ty1 ty2 => tApp T⟦ty1⟧ T⟦ty2⟧
   | tyArr ty1 ty2 =>
@@ -84,7 +84,7 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   | eRel i => tRel i
   | eVar nm => tVar (TCString.of_string nm)
   | eLambda nm ty b => tLambda (aRelevant (nNamed (TCString.of_string nm))) T⟦ty⟧ t⟦b⟧Σ
-  | eTyLam nm b => tLambda (aRelevant (nNamed (TCString.of_string nm))) (tSort Universe.type0) t⟦b⟧Σ
+  | eTyLam nm b => tLambda (aRelevant (nNamed (TCString.of_string nm))) (tSort Sort.type0) t⟦b⟧Σ
   | eLetIn nm e1 ty e2 => tLetIn (aRelevant (nNamed (TCString.of_string nm))) t⟦e1⟧Σ T⟦ty⟧ t⟦e2⟧Σ
   | eApp e1 e2 => tApp t⟦e1⟧Σ t⟦e2⟧Σ
   | eConstr i t =>
@@ -175,7 +175,7 @@ Definition trans_one_constr (ind_name : ename) (nparam : nat) (c : constr) : ter
 Fixpoint gen_params n := match n with
                          | O => []
                          | S n' => let nm := ("A" ++ string_of_nat n)%bs in
-                                  let decl := (tSort Universe.type0) in
+                                  let decl := (tSort Sort.type0) in
                                   gen_params n' ++ [mkdecl (aRelevant (nNamed nm)) None (decl)]
                          end.
 
@@ -185,7 +185,7 @@ Definition trans_global_dec (gd : global_dec) : mutual_inductive_entry :=
     let (mp,unqualified_nm) := kername_of_string nm in
     let oie := {|
           mind_entry_typename := unqualified_nm;
-          mind_entry_arity := tSort Universe.type0;
+          mind_entry_arity := tSort Sort.type0;
           mind_entry_template := false;
           mind_entry_consnames :=
             map (fun c => let (mp,unqualified_nm) := kername_of_string c.1 in
diff --git a/extraction/theories/CameLIGOPretty.v b/extraction/theories/CameLIGOPretty.v
index 43b0d271..6dec25b9 100644
--- a/extraction/theories/CameLIGOPretty.v
+++ b/extraction/theories/CameLIGOPretty.v
@@ -722,6 +722,8 @@ Section PPTerm.
     | tFix _ _ => fun _ => "NotSupportedMutualFix"
     | tCoFix l n => fun _ => "NotSupportedCoFix"
     | tPrim _ => fun _ => "NotSupportedCoqPrimitive"
+    | tLazy _ => fun _ => "NotSupportedLazy"
+    | tForce _ => fun _ => "NotSupportedForce"
   end.
 
 End PPTerm.
diff --git a/extraction/theories/LiquidityPretty.v b/extraction/theories/LiquidityPretty.v
index 62b92a49..54482136 100644
--- a/extraction/theories/LiquidityPretty.v
+++ b/extraction/theories/LiquidityPretty.v
@@ -697,6 +697,8 @@ Definition get_record_projs (oib : ExAst.one_inductive_body) : list string :=
     end
   | tCoFix l n => "NotSupportedCoFix"
   | tPrim _ => "NotSupportedCoqPrimitive"
+  | tLazy _ => "NotSupportedLazy"
+  | tForce _ => "NotSupportedForce"
   end.
 
 End print_term.

From f2e11b2dda3fac38a4c1a7ec4ad71d995528bd2e Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Tue, 18 Jun 2024 20:42:21 +0200
Subject: [PATCH 03/10] Port ConCert examples to MetaCoq 1.3.1

---
 .../extraction/CounterRefTypesMidlang.v       | 11 +++++----
 examples/eip20/EIP20TokenCorrect.v            | 24 +++++++++++--------
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/examples/counter/extraction/CounterRefTypesMidlang.v b/examples/counter/extraction/CounterRefTypesMidlang.v
index 21c4ed17..b5cb0344 100644
--- a/examples/counter/extraction/CounterRefTypesMidlang.v
+++ b/examples/counter/extraction/CounterRefTypesMidlang.v
@@ -138,7 +138,7 @@ Definition extract_within_coq : extract_template_env_params :=
           extract_transforms := [dearg_transform (fun _ => None) true false true true true] |} |}.
 
 Definition counter_extract :=
-    Eval vm_compute in
+  Eval vm_compute in
     extract_template_env extract_within_coq
       counter_env
       (KernameSet.singleton counter_name)
@@ -147,10 +147,11 @@ Definition counter_extract :=
                                  ++ map fst midlang_translation_map
                                  ++ map fst TT)).
 
-Definition counter_result := Eval compute in
-     (env <- counter_extract ;;
-      '(_, lines) <- finish_print_lines (print_env env midlang_counter_translate);;
-      ret lines).
+Definition counter_result :=
+  Eval compute in
+    (env <- counter_extract ;;
+    '(_, lines) <- finish_print_lines (print_env env midlang_counter_translate);;
+    ret lines).
 
 Definition wrap_in_delimiters s :=
   concat Common.nl [""; "{-START-} "; s; "{-END-}"].
diff --git a/examples/eip20/EIP20TokenCorrect.v b/examples/eip20/EIP20TokenCorrect.v
index 6599fa64..49d4c049 100644
--- a/examples/eip20/EIP20TokenCorrect.v
+++ b/examples/eip20/EIP20TokenCorrect.v
@@ -150,17 +150,17 @@ Section Theories.
 
   Ltac FMap_simpl_step :=
     match goal with
-      | |- context [ FMap.find ?x (FMap.add ?x _ _) ] => setoid_rewrite FMap.find_add
+      | |- context [ FMap.find ?x (FMap.add ?x _ _) ] => rewrite FMap.find_add
       | H : FMap.find ?t ?m = Some _ |- FMap.find ?t ?m = Some _ => cbn; rewrite H; f_equal; lia
-      | H : ?x <> ?y |- context [ FMap.find ?x (FMap.add ?y _ _) ] => setoid_rewrite FMap.find_add_ne; eauto
-      | H : ?y <> ?x |- context [ FMap.find ?x (FMap.add ?y _ _) ] => setoid_rewrite FMap.find_add_ne; eauto
-      | H : FMap.find ?x _ = Some _ |- context [ FMap.elements (FMap.add ?x _ _) ] => setoid_rewrite FMap.elements_add_existing; eauto
-      | |- context [ FMap.add ?x _ (FMap.add ?x _ _) ] => setoid_rewrite FMap.add_add
-      | H : FMap.find ?x _ = None |- context [ FMap.elements (FMap.add ?x _ _) ] => setoid_rewrite FMap.elements_add; eauto
+      | H : ?x <> ?y |- context [ FMap.find ?x (FMap.add ?y _ _) ] => rewrite FMap.find_add_ne; eauto
+      | H : ?y <> ?x |- context [ FMap.find ?x (FMap.add ?y _ _) ] => rewrite FMap.find_add_ne; eauto
+      | H : FMap.find ?x _ = Some _ |- context [ FMap.elements (FMap.add ?x _ _) ] => rewrite FMap.elements_add_existing; eauto
+      | |- context [ FMap.add ?x _ (FMap.add ?x _ _) ] => rewrite FMap.add_add
+      | H : FMap.find ?x _ = None |- context [ FMap.elements (FMap.add ?x _ _) ] => rewrite FMap.elements_add; eauto
       | |- context [ FMap.remove ?x (FMap.add ?x _ _) ] => rewrite fin_maps.delete_insert_delete
-      | |- context [ FMap.find ?x (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter
-      | H : ?x' <> ?x |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter_ne; auto
-      | H : ?x <> ?x' |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter_ne
+      | |- context [ FMap.find ?x (FMap.partial_alter _ ?x _) ] => rewrite FMap.find_partial_alter
+      | H : ?x' <> ?x |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => rewrite FMap.find_partial_alter_ne; auto
+      | H : ?x <> ?x' |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => rewrite FMap.find_partial_alter_ne
       | H : context [ AddressMap.find _ _ ] |- _ => rewrite AddressMap_find_convertible in H
       | H : context [ AddressMap.add _ _ _ ] |- _ => rewrite AddressMap_add_convertible in H
       | H : context [ increment_balance _ _ _ ] |- _ => rewrite increment_balanace_is_partial_alter_plus in H
@@ -665,6 +665,9 @@ Section Theories.
   Qed.
 
 
+  Remove Hints MCRelations.on_rel_refl : typeclass_instances.
+  Remove Hints MCRelations.on_rel_trans : typeclass_instances.
+  Remove Hints MCRelations.on_rel_sym : typeclass_instances.
 
   (** ** Sum of balances always equals total supply *)
   Lemma sum_balances_eq_total_supply bstate caddr :
@@ -680,7 +683,8 @@ Section Theories.
       inversion_clear init_some.
       unfold sum_balances.
       setoid_rewrite FMap.elements_add; auto.
-      setoid_rewrite FMap.elements_empty. cbn. lia.
+
+      rewrite FMap.elements_empty. cbn. lia.
     - intros IH receive_some.
       unfold Blockchain.receive in *.
       cbn in *.

From 345d8d2a28bf3f5fd0bf5e0e297e0bca600f3fb5 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:10:54 +0200
Subject: [PATCH 04/10] Update opam lock file

---
 .github/coq-concert.opam.locked | 18 +++++++++---------
 coq-concert.opam                | 18 +++++++++---------
 2 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
index 11e12997..bbf61479 100644
--- a/.github/coq-concert.opam.locked
+++ b/.github/coq-concert.opam.locked
@@ -12,13 +12,13 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
   "coq" {= "8.18.0"}
   "coq-bignums" {= "9.0.0+coq8.18"}
-  "coq-metacoq-common" {= "1.2.1+8.18"}
-  "coq-metacoq-erasure" {= "1.2.1+8.18"}
-  "coq-metacoq-pcuic" {= "1.2.1+8.18"}
-  "coq-metacoq-safechecker" {= "1.2.1+8.18"}
-  "coq-metacoq-template" {= "1.2.1+8.18"}
-  "coq-metacoq-template-pcuic" {= "1.2.1+8.18"}
-  "coq-metacoq-utils" {= "1.2.1+8.18"}
+  "coq-metacoq-common" {= "1.3.1+8.18"}
+  "coq-metacoq-erasure" {= "1.3.1+8.18"}
+  "coq-metacoq-pcuic" {= "1.3.1+8.18"}
+  "coq-metacoq-safechecker" {= "1.3.1+8.18"}
+  "coq-metacoq-template" {= "1.3.1+8.18"}
+  "coq-metacoq-template-pcuic" {= "1.3.1+8.18"}
+  "coq-metacoq-utils" {= "1.3.1+8.18"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
   "coq-quickchick" {= "2.0.4"}
@@ -37,10 +37,10 @@ dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"
 pin-depends: [
   [
     "coq-rust-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#0053733e56008c917bf43d12e8bf0616d3b9a856"
+    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#7a5e27c1242abf36cf265e170562a057ac3415f6"
   ]
   [
     "coq-elm-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#903320120e3f36d7857161e5680fabeb6e743c6b"
+    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#32eff8eefebc9b2b7fe81c2653559a819740058b"
   ]
 ]
diff --git a/coq-concert.opam b/coq-concert.opam
index fe4f9fe5..a6e472cd 100644
--- a/coq-concert.opam
+++ b/coq-concert.opam
@@ -17,21 +17,21 @@ depends: [
   "coq" {>= "8.17" & < "8.19~"}
   "coq-bignums" {>= "8"}
   "coq-quickchick" {>= "2.0.4"}
-  "coq-metacoq-utils" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-common" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-template" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-template-pcuic" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-pcuic" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-safechecker" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-erasure" {>= "1.2" & < "1.3~"}
+  "coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-common" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-template" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-template-pcuic" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-pcuic" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-safechecker" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-erasure" {>= "1.3.1" & < "1.4~"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
   "coq-stdpp" {= "1.9.0"}
 ]
 
 pin-depends: [
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#0053733e56008c917bf43d12e8bf0616d3b9a856"]
-  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#903320120e3f36d7857161e5680fabeb6e743c6b"]
+  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#7a5e27c1242abf36cf265e170562a057ac3415f6"]
+  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#32eff8eefebc9b2b7fe81c2653559a819740058b"]
 ]
 
 build: [

From afc60ddfd6c16c0418887dc51f97b5add3c553b4 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:12:41 +0200
Subject: [PATCH 05/10] Update stdpp to 1.10.0

---
 .github/coq-concert.opam.locked                  | 2 +-
 coq-concert.opam                                 | 2 +-
 embedding/extraction/PreludeExt.v                | 4 ++--
 examples/crowdfunding/ExecFrameworkIntegration.v | 2 +-
 execution/theories/BuildUtils.v                  | 2 +-
 execution/theories/Containers.v                  | 6 ++++--
 execution/theories/Serializable.v                | 2 ++
 7 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
index bbf61479..9d1eaba7 100644
--- 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" {= "2.0.4"}
-  "coq-stdpp" {= "1.9.0"}
+  "coq-stdpp" {= "1.10.0"}
 ]
 build: [
   [make]
diff --git a/coq-concert.opam b/coq-concert.opam
index a6e472cd..32864316 100644
--- 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
index 2ede454d..3c1e3779 100644
--- 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
index a3c71a63..85c7852f 100644
--- 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
index c2b14e43..67f65f2f 100644
--- 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
index 0ef823ef..628e6c15 100644
--- 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
index 22b2a23f..20b2b9a4 100644
--- 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.

From b015a0adc6cdfe20f1590d5591e24cad3b7e4a5c Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:14:37 +0200
Subject: [PATCH 06/10] Support Coq 8.19

---
 .github/coq-concert.opam.locked                | 18 +++++++++---------
 coq-concert.opam                               |  2 +-
 examples/boardroomVoting/BoardroomVotingTest.v |  3 ++-
 3 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
index 9d1eaba7..6f3b92ee 100644
--- a/.github/coq-concert.opam.locked
+++ b/.github/coq-concert.opam.locked
@@ -10,15 +10,15 @@ homepage: "https://github.com/AU-COBRA/ConCert"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
-  "coq" {= "8.18.0"}
-  "coq-bignums" {= "9.0.0+coq8.18"}
-  "coq-metacoq-common" {= "1.3.1+8.18"}
-  "coq-metacoq-erasure" {= "1.3.1+8.18"}
-  "coq-metacoq-pcuic" {= "1.3.1+8.18"}
-  "coq-metacoq-safechecker" {= "1.3.1+8.18"}
-  "coq-metacoq-template" {= "1.3.1+8.18"}
-  "coq-metacoq-template-pcuic" {= "1.3.1+8.18"}
-  "coq-metacoq-utils" {= "1.3.1+8.18"}
+  "coq" {= "8.19.0"}
+  "coq-bignums" {= "9.0.0+coq8.19"}
+  "coq-metacoq-common" {= "1.3.1+8.19"}
+  "coq-metacoq-erasure" {= "1.3.1+8.19"}
+  "coq-metacoq-pcuic" {= "1.3.1+8.19"}
+  "coq-metacoq-safechecker" {= "1.3.1+8.19"}
+  "coq-metacoq-template" {= "1.3.1+8.19"}
+  "coq-metacoq-template-pcuic" {= "1.3.1+8.19"}
+  "coq-metacoq-utils" {= "1.3.1+8.19"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
   "coq-quickchick" {= "2.0.4"}
diff --git a/coq-concert.opam b/coq-concert.opam
index 32864316..bfe547b0 100644
--- a/coq-concert.opam
+++ b/coq-concert.opam
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 
 depends: [
-  "coq" {>= "8.17" & < "8.19~"}
+  "coq" {>= "8.17" & < "8.20~"}
   "coq-bignums" {>= "8"}
   "coq-quickchick" {>= "2.0.4"}
   "coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}
diff --git a/examples/boardroomVoting/BoardroomVotingTest.v b/examples/boardroomVoting/BoardroomVotingTest.v
index ec16eeac..f30b710e 100644
--- a/examples/boardroomVoting/BoardroomVotingTest.v
+++ b/examples/boardroomVoting/BoardroomVotingTest.v
@@ -1,4 +1,5 @@
-From Coq Require Import Cyclic31.
+(* From Coq Require Import Cyclic31. *)
+From Coq.Numbers.Cyclic.Int63 Require Import Cyclic63.
 From Coq Require Import List.
 From Coq Require Import Znumtheory.
 From ConCert.Utils Require Import Extras.

From b9530d20587741e1fcc3ba0c00892005854ddee0 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:16:54 +0200
Subject: [PATCH 07/10] Use rust and elm extraction 0.1.0 releases

---
 .github/coq-concert.opam.locked | 14 ++------------
 coq-concert.opam                |  9 ++-------
 2 files changed, 4 insertions(+), 19 deletions(-)

diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
index 6f3b92ee..9ae60eb5 100644
--- a/.github/coq-concert.opam.locked
+++ b/.github/coq-concert.opam.locked
@@ -19,8 +19,8 @@ depends: [
   "coq-metacoq-template" {= "1.3.1+8.19"}
   "coq-metacoq-template-pcuic" {= "1.3.1+8.19"}
   "coq-metacoq-utils" {= "1.3.1+8.19"}
-  "coq-rust-extraction" {= "dev"}
-  "coq-elm-extraction" {= "dev"}
+  "coq-rust-extraction" {= "0.1.0"}
+  "coq-elm-extraction" {= "0.1.0"}
   "coq-quickchick" {= "2.0.4"}
   "coq-stdpp" {= "1.10.0"}
 ]
@@ -34,13 +34,3 @@ install: [
   [make "-C" "examples" "install"] {with-test}
 ]
 dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"
-pin-depends: [
-  [
-    "coq-rust-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#7a5e27c1242abf36cf265e170562a057ac3415f6"
-  ]
-  [
-    "coq-elm-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#32eff8eefebc9b2b7fe81c2653559a819740058b"
-  ]
-]
diff --git a/coq-concert.opam b/coq-concert.opam
index bfe547b0..ad8db225 100644
--- a/coq-concert.opam
+++ b/coq-concert.opam
@@ -24,16 +24,11 @@ depends: [
   "coq-metacoq-pcuic" {>= "1.3.1" & < "1.4~"}
   "coq-metacoq-safechecker" {>= "1.3.1" & < "1.4~"}
   "coq-metacoq-erasure" {>= "1.3.1" & < "1.4~"}
-  "coq-rust-extraction" {= "dev"}
-  "coq-elm-extraction" {= "dev"}
+  "coq-rust-extraction" {= "0.1.0"}
+  "coq-elm-extraction" {= "0.1.0"}
   "coq-stdpp" {>= "1.9.0" & < "1.11~"}
 ]
 
-pin-depends: [
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#7a5e27c1242abf36cf265e170562a057ac3415f6"]
-  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#32eff8eefebc9b2b7fe81c2653559a819740058b"]
-]
-
 build: [
   [make]
   [make "examples"] {with-test}

From 36da1bdf1e5497b8da143a924c9263c0ff0bb8e7 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Thu, 16 Jan 2025 17:25:36 +0100
Subject: [PATCH 08/10] Pin MetaCoq 8.19 branch

---
 .github/coq-concert.opam.locked            | 23 +++++++++++++++-------
 coq-concert.opam                           | 10 ++++++++++
 extraction/tests/CameLIGOExtractionTests.v |  2 ++
 3 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
index 9ae60eb5..1eb968bc 100644
--- a/.github/coq-concert.opam.locked
+++ b/.github/coq-concert.opam.locked
@@ -12,18 +12,27 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
   "coq" {= "8.19.0"}
   "coq-bignums" {= "9.0.0+coq8.19"}
-  "coq-metacoq-common" {= "1.3.1+8.19"}
-  "coq-metacoq-erasure" {= "1.3.1+8.19"}
-  "coq-metacoq-pcuic" {= "1.3.1+8.19"}
-  "coq-metacoq-safechecker" {= "1.3.1+8.19"}
-  "coq-metacoq-template" {= "1.3.1+8.19"}
-  "coq-metacoq-template-pcuic" {= "1.3.1+8.19"}
-  "coq-metacoq-utils" {= "1.3.1+8.19"}
+  "coq-metacoq-common" {= "1.3.2+8.19"}
+  "coq-metacoq-erasure" {= "1.3.2+8.19"}
+  "coq-metacoq-pcuic" {= "1.3.2+8.19"}
+  "coq-metacoq-safechecker" {= "1.3.2+8.19"}
+  "coq-metacoq-template" {= "1.3.2+8.19"}
+  "coq-metacoq-template-pcuic" {= "1.3.2+8.19"}
+  "coq-metacoq-utils" {= "1.3.2+8.19"}
   "coq-rust-extraction" {= "0.1.0"}
   "coq-elm-extraction" {= "0.1.0"}
   "coq-quickchick" {= "2.0.4"}
   "coq-stdpp" {= "1.10.0"}
 ]
+pin-depends: [
+  ["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+]
 build: [
   [make]
   [make "examples"] {with-test}
diff --git a/coq-concert.opam b/coq-concert.opam
index ad8db225..b095e379 100644
--- a/coq-concert.opam
+++ b/coq-concert.opam
@@ -29,6 +29,16 @@ depends: [
   "coq-stdpp" {>= "1.9.0" & < "1.11~"}
 ]
 
+pin-depends: [
+  ["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+]
+
 build: [
   [make]
   [make "examples"] {with-test}
diff --git a/extraction/tests/CameLIGOExtractionTests.v b/extraction/tests/CameLIGOExtractionTests.v
index 818af979..f63b387e 100644
--- a/extraction/tests/CameLIGOExtractionTests.v
+++ b/extraction/tests/CameLIGOExtractionTests.v
@@ -12,6 +12,8 @@ From Coq Require Import String.
 
 Import MCMonadNotation.
 
+Context `{Blockchain.ChainBase}.
+
 Local Close Scope bs_scope.
 Local Open Scope string_scope.
 

From 8f95a2c9f7fe514a2ede800552810b926cfb3166 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Thu, 16 Jan 2025 19:53:35 +0100
Subject: [PATCH 09/10] Remove support for Coq 8.17 and 8.18

---
 coq-concert.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq-concert.opam b/coq-concert.opam
index b095e379..5ba4bd18 100644
--- a/coq-concert.opam
+++ b/coq-concert.opam
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 
 depends: [
-  "coq" {>= "8.17" & < "8.20~"}
+  "coq" {>= "8.19" & < "8.20~"}
   "coq-bignums" {>= "8"}
   "coq-quickchick" {>= "2.0.4"}
   "coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}

From 9bcb14ad49b3cba1487e3903f4d9965514f9f62e Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Thu, 16 Jan 2025 19:55:52 +0100
Subject: [PATCH 10/10] Update readme

---
 README.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 79cac5d5..57ad9b6a 100644
--- a/README.md
+++ b/README.md
@@ -13,7 +13,7 @@ ConCert can find real-world attacks as explained
 
 ## How to build
 
-Our development works with Coq 8.17 and depends on MetaCoq, and std++.
+Our development works with Coq 8.19 and depends on MetaCoq, and std++.
 The tests depend on QuickChick.
 The dependencies can be installed through `opam`.
 
@@ -21,11 +21,11 @@ Branches compatible with older versions of Coq can be found [here](https://githu
 
 ### Install dependencies and build ConCert locally
 
-Installing the necessary dependencies requires the opam package manager and a switch with Coq 8.17 installed.
+Installing the necessary dependencies requires the opam package manager and a switch with Coq 8.19 installed.
 If you don't already have a switch set up run the following commands
 
 ```bash
-opam switch create . 4.10.2 --repositories default,coq-released=https://coq.inria.fr/opam/released
+opam switch create . 4.14.2 --repositories default,coq-released=https://coq.inria.fr/opam/released
 eval $(opam env)
 ```