diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-11-05 18:03:52 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-11-05 18:03:52 +0000 |
| commit | 7d0a4d8c93d47a076f58a9ec6ad0cbba100c79a1 (patch) | |
| tree | c2ec7abfce56f3fcfc1398f02f26754a2533a884 /theories/Arith/Wf_nat.v | |
| parent | af0e34649ea94994fcdbf9b39ae78af21842a794 (diff) | |
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
Diffstat (limited to 'theories/Arith/Wf_nat.v')
| -rw-r--r-- | theories/Arith/Wf_nat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 8e26942d1..7e85e5c67 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. |