blob: 5a548cfae41b0d08c3b3edc77b3abe4551534911 (
plain)
1
2
3
4
5
6
7
8
|
The command has indeed failed with message:
Last occurrence of "list'" must have "A" as 1st argument in
"A -> list' A -> list' (A * A)".
Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=
Foo : foo A x
For foo: Argument scopes are [type_scope _]
For Foo: Argument scopes are [type_scope _]
|
