diff options
Diffstat (limited to 'theories/micromega/Lia.v')
| -rw-r--r-- | theories/micromega/Lia.v | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index e53800d07d..5d97fc46ef 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -14,11 +14,8 @@ (* *) (************************************************************************) -Require Import ZMicromega. -Require Import ZArith_base. -Require Import RingMicromega. -Require Import VarMap. -Require Import DeclConstant. +Require Import ZMicromega RingMicromega VarMap DeclConstant. +Require Import BinNums. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". @@ -29,9 +26,9 @@ Ltac zchecker := (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true) (@find Z Z0 __varmap)). -Ltac lia := PreOmega.zify; xlia zchecker. +Ltac lia := Zify.zify; xlia zchecker. -Ltac nia := PreOmega.zify; xnlia zchecker. +Ltac nia := Zify.zify; xnlia zchecker. (* Local Variables: *) |