From 46a88cb66d66092fcb4434baf865248fcb43efcc Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Fri, 2 Aug 2024 09:57:07 +0200
Subject: [PATCH] adapt to MC#1229

---
 refinements/binord.v |  2 +-
 refinements/boolF2.v | 24 +++++++++++-------------
 2 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/refinements/binord.v b/refinements/binord.v
index 75f4870..2fd0d6e 100644
--- a/refinements/binord.v
+++ b/refinements/binord.v
@@ -118,7 +118,7 @@ Local Arguments mul_ord /.
 
 #[export] Instance Rord_mul n1 n2 (rn : nat_R n1 n2) :
   refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn))
-          (@Zp_mul n1) *%C.
+  (@Zp_mul _) *%C.
 Proof.
   rewrite refinesE=> x x' hx y y' hy /=.
   exact: refinesP.
diff --git a/refinements/boolF2.v b/refinements/boolF2.v
index 571c2d2..45c715f 100644
--- a/refinements/boolF2.v
+++ b/refinements/boolF2.v
@@ -44,42 +44,40 @@ Proof. by rewrite refinesE. Qed.
 
 #[export] Instance Rbool_opp : refines (Rbool ==> Rbool) -%R -%C.
 Proof.
-rewrite refinesE=> x []; rewrite /Rbool /F2_of_bool /fun_hrel /= => <- //.
-by rewrite GRing.mulr0n GRing.oppr0.
+rewrite refinesE => x.
+by case; rewrite /Rbool /F2_of_bool /fun_hrel /= => <-; apply/val_inj.
 Qed.
 
 #[export] Instance Rbool_add : refines (Rbool ==> Rbool ==> Rbool) +%R +%C.
 Proof.
-rewrite refinesE /Rbool /F2_of_bool /fun_hrel => x [] <- y [] <- //=.
-  by rewrite -GRing.natrD char_Zp.
-by rewrite GRing.add0r.
+rewrite refinesE /Rbool /F2_of_bool /fun_hrel.
+by move=> x [] <- y [] <-; apply/val_inj.
 Qed.
 
 (* TODO: lemma for sub *)
 #[export] Instance Rbool_sub :
   refines (Rbool ==> Rbool ==> Rbool) (fun x y => x - y) sub_op.
 Proof.
-  rewrite refinesE /Rbool /F2_of_bool /fun_hrel=> x [] <- y [] <- //=;
-  by apply/eqP; rewrite eq_sym GRing.subr_eq0.
+rewrite refinesE /Rbool /F2_of_bool /fun_hrel.
+by move=> x [] <- y [] <-; apply/val_inj.
 Qed.
 
 #[export] Instance Rbool_mul : refines (Rbool ==> Rbool ==> Rbool) *%R *%C.
 Proof.
-rewrite refinesE /Rbool /F2_of_bool /fun_hrel => x [] <- y [] <- //=.
-+ by rewrite GRing.mulr0.
-+ by rewrite GRing.mul0r.
-by rewrite GRing.mul0r.
+rewrite refinesE /Rbool /F2_of_bool /fun_hrel.
+by move=> x [] <- y [] <-; apply/val_inj.
 Qed.
 
 #[export] Instance Rbool_inv : refines (Rbool ==> Rbool) GRing.inv inv_bool.
 Proof.
-by rewrite refinesE=> x []; rewrite /Rbool /F2_of_bool /fun_hrel /= => <- //.
+rewrite refinesE => x.
+by case; rewrite /Rbool /F2_of_bool /fun_hrel /= => <-; apply/val_inj.
 Qed.
 
 #[export] Instance Rbool_eq :
   refines (Rbool ==> Rbool ==> bool_R) eqtype.eq_op eq_op.
 Proof.
-  by rewrite refinesE /Rbool /F2_of_bool /fun_hrel=> x [] <- y [] <-.
+by rewrite refinesE /Rbool /F2_of_bool /fun_hrel=> x [] <- y [] <-.
 Qed.
 
 (*