Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the

opportunity to extend the class of singleton types to (possibly mutual)
recursive types with single constructors of which all arguments are in
Prop. This covers Acc. Acc_rect can consequently be defined in the
direct way.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11249 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 16 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index ff079a0eee..2d35a4b237 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -27,6 +27,7 @@ Section Well_founded.
  Variable R : A -> A -> Prop.
 
  (** The accessibility predicate is defined to be non-informative *)
+ (** (Acc_rect is automatically defined because Acc is a singleton type) *)
 
  Inductive Acc (x: A) : Prop :=
      Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
@@ -35,22 +36,6 @@ Section Well_founded.
   destruct 1; trivial.
  Defined.
 
-  (** Informative elimination :
-     [let Acc_rec F = let rec wf x = F x wf in wf] *)
-
- Section AccRecType.
-
-  Variable P : A -> Type.
-  Variable F : forall x:A,
-    (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
-
-  Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
-    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (Acc_inv a h)).
-
- End AccRecType.
-
- Definition Acc_rec (P:A -> Set) := Acc_rect P.
-
  (** A relation is well-founded if every element is accessible *)
 
  Definition well_founded := forall a:A, Acc a.