From 7d0a4d8c93d47a076f58a9ec6ad0cbba100c79a1 Mon Sep 17 00:00:00 2001
From: bertot
Date: Sun, 5 Nov 2006 18:03:52 +0000
Subject: fixes PR#1269 about function: there is no reason well founded
 induction is limited to only Set and not any type in Type

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

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 8e26942d10..7e85e5c67b 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -18,7 +18,7 @@ Implicit Types m n p : nat.
 
 Section Well_founded_Nat.
 
-Variable A : Set.
+Variable A : Type.
 
 Variable f : A -> nat.
 Definition ltof (a b:A) := f a < f b.
-- 
cgit v1.2.3