From 9b2ebb8556e6804f5c7490f0a63350487652fc73 Mon Sep 17 00:00:00 2001
From: roconnor
Date: Wed, 23 Jan 2008 22:08:35 +0000
Subject: Changing R to a local definition so that it isn't exported.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10470 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/ConstructiveEpsilon.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 98260c7fc1..36ff2681b5 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -49,7 +49,7 @@ numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after
 infinite [R]-descending chain from 0 is equivalent to the termination
 of our searching algorithm. *)
 
-Definition R (x y : nat) : Prop := x = S y /\ ~ P y.
+Let R (x y : nat) : Prop := x = S y /\ ~ P y.
 
 Notation Local "'acc' x" := (Acc R x) (at level 10).
 
-- 
cgit v1.2.3