aboutsummaryrefslogtreecommitdiff
path: root/src/LegacyArithmetic/ZBoundedZ.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/LegacyArithmetic/ZBoundedZ.v')
-rw-r--r--src/LegacyArithmetic/ZBoundedZ.v8
1 files changed, 4 insertions, 4 deletions
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. }