The Coq mailing list

["Daniel R. Grayson"<drg AT illinois.edu>]

The trunk generates one more inductive principle than 8.3 did, but the new one
(*_case) seems often to be the same as one of the old ones (*_rect).  The
reference manual doesn't explain its purpose.  Can anyone clarify?

 >>>>>>> Library Top
Inductive paths (A : Type (* Top.1 *)) : A -> A -> Type (* Top.1 *) :=
    idpath : forall x : A, @paths A x x

For paths: Argument A is implicit and maximally inserted
For idpath: Argument A is implicit and maximally inserted
For paths: Argument scopes are [type_scope _ _]
For idpath: Argument scopes are [type_scope _]

paths_rect : 
forall (A : Type (* Top.3 *))
  (P : forall a a0 : A, @paths A a a0 -> Type (* Top.4 *)),
(forall x : A, P x x (@idpath A x)) ->
forall (y y0 : A) (p : @paths A y y0), P y y0 p

paths_ind : 
forall (A : Type (* Top.3 *)) (P : forall a a0 : A, @paths A a a0 -> Prop),
(forall x : A, P x x (@idpath A x)) ->
forall (y y0 : A) (p : @paths A y y0), P y y0 p

paths_rec : 
forall (A : Type (* Top.3 *)) (P : forall a a0 : A, @paths A a a0 -> Set),
(forall x : A, P x x (@idpath A x)) ->
forall (y y0 : A) (p : @paths A y y0), P y y0 p

paths_case : 
forall (A : Type (* Top.5 *))
  (P : forall a a0 : A, @paths A a a0 -> Type (* Top.6 *)),
(forall x : A, P x x (@idpath A x)) ->
forall (y y0 : A) (p : @paths A y y0), P y y0 p