From f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:09 +0000 Subject: Definitions of positive, N, Z moved in Numbers/BinNums.v In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/ZMicromega.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/micromega/ZMicromega.v') diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index c8d324730..ab63f7bf0 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -194,7 +194,7 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z) := | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil end. -Require Import Tauto. +Require Import Tauto BinNums. Definition normalise (t:Formula Z) : cnf (NFormula Z) := List.map (fun x => x::nil) (xnormalise t). -- cgit v1.2.3