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/RMicromega.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/micromega/RMicromega.v') diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 72353a99e..2352d78d6 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -533,7 +533,7 @@ Proof. exact H. Qed. -Require Import Tauto. +Require Import Coq.micromega.Tauto. Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool. Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool. -- cgit v1.2.3