blob: ff2556c5dc1ea0c3f28e5cb1d6861a7404c77ed8 (
plain)
1
2
3
4
5
6
7
8
9
|
The command has indeed failed with message:
Last occurrence of "list'" must have "A" as 1st argument in
"A -> list' A -> list' (A * A)%type".
Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x
Arguments foo _%type_scope
Arguments Foo _%type_scope
myprod unit bool
: Set
|
