Port ConCert examples to MetaCoq 1.3.1

AU-COBRA · Jun 18, 2024 · af78d2e · af78d2e
1 parent bd2aba2
commit af78d2e
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 15 deletions.
diff --git a/examples/counter/extraction/CounterRefTypesMidlang.v b/examples/counter/extraction/CounterRefTypesMidlang.v
@@ -141,7 +141,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)
@@ -150,10 +150,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
@@ -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 *.