From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- theories/ZArith/Zmin.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'theories/ZArith/Zmin.v') 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). -- cgit v1.2.3