From f0168fd8ce775b0a96e8cf026e953e9d55f4de25 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 21 Oct 2010 06:48:00 +0000 Subject: Solve name conflict about pow introduced by commit 13546. - NPeano isn't Exported by default anymore (contains pow for nat). - in coq_micromega.ml, we specify more where to find the pow of R. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13569 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Arith/Max.v | 2 +- theories/Arith/Min.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Arith') diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 2022331bb..77dfa5080 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,7 +8,7 @@ (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) -Require Export NPeano. +Require Import NPeano. Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 742c8126c..2b2cf860d 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -8,7 +8,7 @@ (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) -Require Export NPeano. +Require Import NPeano. Open Local Scope nat_scope. Implicit Types m n p : nat. -- cgit v1.2.3