diff options
Diffstat (limited to 'contrib/omega/Omega.v')
| -rwxr-xr-x | contrib/omega/Omega.v | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 480f7594be..e381b1fbeb 100755 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -19,9 +19,9 @@ Require Export ZArith_base. Require Export OmegaLemmas. -Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc - Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r - Zmult_plus_distr_l Zmult_plus_distr_r : zarith. +Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l + Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l + Zmult_plus_distr_r: zarith. Require Export Zhints. @@ -30,28 +30,28 @@ Require Export Zhints. Require Minus. *) -Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega. -Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega. -Hint lt_Omega : zarith := Extern 10 (lt ? ?) Abstract Omega. -Hint ge_Omega : zarith := Extern 10 (ge ? ?) Abstract Omega. -Hint gt_Omega : zarith := Extern 10 (gt ? ?) Abstract Omega. - -Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq nat ? ?) Abstract Omega. -Hint not_le_Omega : zarith := Extern 10 ~(le ? ?) Abstract Omega. -Hint not_lt_Omega : zarith := Extern 10 ~(lt ? ?) Abstract Omega. -Hint not_ge_Omega : zarith := Extern 10 ~(ge ? ?) Abstract Omega. -Hint not_gt_Omega : zarith := Extern 10 ~(gt ? ?) Abstract Omega. - -Hint eq_Z_Omega : zarith := Extern 10 (eq Z ? ?) Abstract Omega. -Hint Zle_Omega : zarith := Extern 10 (Zle ? ?) Abstract Omega. -Hint Zlt_Omega : zarith := Extern 10 (Zlt ? ?) Abstract Omega. -Hint Zge_Omega : zarith := Extern 10 (Zge ? ?) Abstract Omega. -Hint Zgt_Omega : zarith := Extern 10 (Zgt ? ?) Abstract Omega. - -Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq Z ? ?) Abstract Omega. -Hint not_Zle_Omega : zarith := Extern 10 ~(Zle ? ?) Abstract Omega. -Hint not_Zlt_Omega : zarith := Extern 10 ~(Zlt ? ?) Abstract Omega. -Hint not_Zge_Omega : zarith := Extern 10 ~(Zge ? ?) Abstract Omega. -Hint not_Zgt_Omega : zarith := Extern 10 ~(Zgt ? ?) Abstract Omega. - -Hint false_Omega : zarith := Extern 10 False Abstract Omega. +Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith. +Hint Extern 10 (_ <= _) => abstract omega: zarith. +Hint Extern 10 (_ < _) => abstract omega: zarith. +Hint Extern 10 (_ >= _) => abstract omega: zarith. +Hint Extern 10 (_ > _) => abstract omega: zarith. + +Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith. +Hint Extern 10 (~ _ <= _) => abstract omega: zarith. +Hint Extern 10 (~ _ < _) => abstract omega: zarith. +Hint Extern 10 (~ _ >= _) => abstract omega: zarith. +Hint Extern 10 (~ _ > _) => abstract omega: zarith. + +Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith. +Hint Extern 10 (_ <= _)%Z => abstract omega: zarith. +Hint Extern 10 (_ < _)%Z => abstract omega: zarith. +Hint Extern 10 (_ >= _)%Z => abstract omega: zarith. +Hint Extern 10 (_ > _)%Z => abstract omega: zarith. + +Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith. + +Hint Extern 10 False => abstract omega: zarith.
\ No newline at end of file |