Do not rely on `Refine Instance Mode`

This option is soon going to be turned off by default. See
https://github.com/coq/coq/pull/9270

2 files changed, 8 insertions, 8 deletions

diff --git a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v
index 5ff67d7ec..899b10162 100644
--- a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v
+++ b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v
@@ -84,11 +84,11 @@ Section fancy_machine_p256_montgomery_foundation.
          (smaller_bound_exp : Z)
          (smaller_bound_smaller : 0 <= smaller_bound_exp <= n)
          (n_pos : 0 < n)
-    : ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps_Factored ops modulus smaller_bound_exp ldi_modulus ldi_0)
-    := { large_valid v := True;
-         medium_valid v := 0 <= decode_large v < 2^n * 2^smaller_bound_exp;
-         small_valid v := True }.
+    : ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps_Factored ops modulus smaller_bound_exp ldi_modulus ldi_0).
   Proof.
+  refine {| large_valid v := True;
+            medium_valid v := 0 <= decode_large v < 2^n * 2^smaller_bound_exp;
+            small_valid v := True |}.
     (* In 8.5: *)
     (* par:t. *)
     { abstract t. }
diff --git a/src/LegacyArithmetic/ZBoundedZ.v b/src/LegacyArithmetic/ZBoundedZ.v
index 2943598c1..f0dfc6a40 100644
--- a/src/LegacyArithmetic/ZBoundedZ.v
+++ b/src/LegacyArithmetic/ZBoundedZ.v
@@ -58,11 +58,11 @@ Global Instance ZZLikeProperties {small_bound_exp smaller_bound_exp modulus}
        {Hs_ss : cls_is_true (smaller_bound_exp <=? small_bound_exp)}
        {Hmod0 : cls_is_true (0 <=? modulus)}
        {Hmod1 : cls_is_true (modulus <? 2^small_bound_exp)}
-  : ZLikeProperties (@ZZLikeOps small_bound_exp smaller_bound_exp modulus)
-  := { large_valid x := 0 <= x < 2^(2*small_bound_exp);
-       medium_valid x := 0 <= x < 2^(small_bound_exp + smaller_bound_exp);
-       small_valid x := 0 <= x < 2^small_bound_exp }.
+  : ZLikeProperties (@ZZLikeOps small_bound_exp smaller_bound_exp modulus).
 Proof.
+refine {| large_valid x := 0 <= x < 2^(2*small_bound_exp);
+          medium_valid x := 0 <= x < 2^(small_bound_exp + smaller_bound_exp);
+          small_valid x := 0 <= x < 2^small_bound_exp |}.
   { abstract t. }
   { abstract t. }
   { abstract t. }