diff options
Diffstat (limited to 'theories/ZArith/Zmin.v')
| -rw-r--r-- | theories/ZArith/Zmin.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 6bc72227..5509ee78 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -18,20 +18,20 @@ Local Open Scope Z_scope. (** Exact compatibility *) -Notation Zmin_case := Z.min_case (compat "8.6"). -Notation Zmin_case_strong := Z.min_case_strong (compat "8.6"). -Notation Zle_min_l := Z.le_min_l (compat "8.6"). -Notation Zle_min_r := Z.le_min_r (compat "8.6"). -Notation Zmin_glb := Z.min_glb (compat "8.6"). -Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.6"). +Notation Zmin_case := Z.min_case (compat "8.7"). +Notation Zmin_case_strong := Z.min_case_strong (compat "8.7"). +Notation Zle_min_l := Z.le_min_l (compat "8.7"). +Notation Zle_min_r := Z.le_min_r (compat "8.7"). +Notation Zmin_glb := Z.min_glb (compat "8.7"). +Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.7"). Notation Zle_min_compat_r := Z.min_le_compat_r (only parsing). Notation Zle_min_compat_l := Z.min_le_compat_l (only parsing). Notation Zmin_idempotent := Z.min_id (only parsing). Notation Zmin_n_n := Z.min_id (only parsing). -Notation Zmin_comm := Z.min_comm (compat "8.6"). -Notation Zmin_assoc := Z.min_assoc (compat "8.6"). +Notation Zmin_comm := Z.min_comm (compat "8.7"). +Notation Zmin_assoc := Z.min_assoc (compat "8.7"). Notation Zmin_irreducible_inf := Z.min_dec (only parsing). -Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.6"). +Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.7"). Notation Zmin_SS := Z.succ_min_distr (only parsing). Notation Zplus_min_distr_r := Z.add_min_distr_r (only parsing). Notation Zmin_plus := Z.add_min_distr_r (only parsing). |