From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/micromega/RingMicromega.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/micromega/RingMicromega.v') diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 751a81df..ed49c3df 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -794,7 +794,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) := | OpLe => (psub lhs rhs ,Strict) :: nil end. -Require Import Tauto. +Require Import Coq.micromega.Tauto. Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). -- cgit v1.2.3