From c14e6eebc6c3696623a440cd7eaa4a8d8fe4f492 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 19 May 2016 13:10:19 +0200 Subject: Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/Tauto.v) --- plugins/micromega/QMicromega.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/micromega/QMicromega.v') diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index 432683635..b13285f53 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -168,7 +168,7 @@ Proof. exact H. Qed. -Require Import Tauto. +Require Import Coq.micromega.Tauto. Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. -- cgit v1.2.3