The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Jonathan,

  Could you please report it on the coq bugzilla (coq.inria.fr/bugs)?
coq-club is not really appropriate for bug reports.

Best,
— Matthieu

On 7 mai 2014, at 05:13, Jonathan 
<jonikelee AT gmail.com>
 wrote:

> Another failure - this possibly pointing to some universe changes:
> 
> Inductive Foo(A : Type) : Prop :=
>   foo: A -> Foo A.
> 
> Arguments foo [A] _.
> 
> Scheme Foo_elim := Induction for Foo Sort Prop.
> 
> Goal forall (fn : Foo nat), { x: nat | foo x = fn }.
> intro fn.
> induction fn as [n] using Foo_elim. (* should fail in a non-Prop context, 
> but now succeeds *)
> exists n.
> reflexivity.
> Qed. (* fails with error  below *)
> (* also note that "undo step" doesn't work once Qed fails *)
> 
> (* The error produced at Qed is:
> Toplevel input, characters 0-4:
> Error: Illegal application: 
> The term "Foo_elim" of type
>  "forall (A : Type) (P : Foo A -> Prop),
>   (forall a : A, P (foo a)) -> forall f0 : Foo A, P f0"
> cannot be applied to the terms
>  "nat" : "Set"
>  "fun f : Foo nat => {x : nat | foo x = f}" : "Foo nat -> Set"
>  "fun n : nat => exist (fun x : nat => foo x = foo n) n eq_refl"
>    : "forall n : nat, {x : nat | foo x = foo n}"
>  "fn" : "Foo nat"
> The 2nd term has type "Foo nat -> Set" which should be coercible to
>  "Foo nat -> Prop".
> *)
>