1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(**************************************************************************)
10
(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
12
(* Pierre Crégut (CNET, Lannion, France) *)
14
(**************************************************************************)
16
(* $Id: Omega.v 10028 2007-07-18 22:38:06Z letouzey $ *)
18
(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
19
Require Export ZArith_base.
20
Require Export OmegaLemmas.
21
Require Export PreOmega.
23
Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
24
Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
25
Zmult_plus_distr_r: zarith.
27
Require Export Zhints.
30
(* The constant minus is required in coq_omega.ml *)
34
Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
35
Hint Extern 10 (_ <= _) => abstract omega: zarith.
36
Hint Extern 10 (_ < _) => abstract omega: zarith.
37
Hint Extern 10 (_ >= _) => abstract omega: zarith.
38
Hint Extern 10 (_ > _) => abstract omega: zarith.
40
Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
41
Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
42
Hint Extern 10 (~ _ < _) => abstract omega: zarith.
43
Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
44
Hint Extern 10 (~ _ > _) => abstract omega: zarith.
46
Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
47
Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
48
Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
49
Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
50
Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
52
Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
53
Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
54
Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
55
Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
56
Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
58
Hint Extern 10 False => abstract omega: zarith.
b'\\ No newline at end of file'