diff options
Diffstat (limited to 'plugins/micromega/ZMicromega.v')
| -rw-r--r-- | plugins/micromega/ZMicromega.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index d7ddef2b..5aa8d03f 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -198,7 +198,7 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z) := | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil end. -Require Import Tauto BinNums. +Require Import Coq.micromega.Tauto BinNums. Definition normalise (t:Formula Z) : cnf (NFormula Z) := List.map (fun x => x::nil) (xnormalise t). |