The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Hi all, I don't understand why the first definition is accepted and not
the second one.

Inductive bool_comp (b: bool): bool -> Prop :=
| Opp: forall q, (if b
                 then match q with true => False | false => True end
                 else match q with true => True | false => False end)
                 -> bool_comp b q.

Print bool_comp.
Inductive bool_comp2 (b: bool): bool -> Prop :=
| Opp2: forall q, (match b return Prop with
                 | true => match q return Prop with true => False |
false => True end | false => match q return Prop with true => True |
false => False end end) -> bool_comp2 b q.