diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 47137414dc..ff1a2b5a53 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1775,8 +1775,6 @@ weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos) Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *) -Register Zne as plugins.omega.Zne. - Ltac elim_compare com1 com2 := case (Dcompare (com1 ?= com2)%Z); [ idtac | let x := fresh "H" in |