The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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".
*)