From 672ba13a7287dc2b6d5a28960deacc4966d364aa Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 8 May 2008 21:19:19 +0000
Subject: remove mention of an obsolete limitation of Add Morphism

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10908 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/NatInt/NZBase.v | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 084560de3b..2e5b585bb3 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -54,12 +54,7 @@ left-inverse to the successor at this point *)
 
 Section CentralInduction.
 
-Variable A : NZ -> Prop.
-
-(* FIXME: declaring "A : predicate NZ" leads to the error during the
-declaration of the morphism below because the "predicate NZ" is not
-recognized as a type of function. Maybe it should do "eval hnf" or
-something like this. The same goes for "relation". *)
+Variable A : predicate NZ.
 
 Hypothesis A_wd : predicate_wd NZeq A.
 
-- 
cgit v1.2.3