The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Cedric,

> 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.

It is a bug ("match" used the matched variable name as internal binder
name in the internal form of the return clause what was not treated by
the test protected against binding hidden implicit arguments of
inductive types as "b" is here).

This can be bypassed by using "match b as b' return ..." instead.

Hugo