The Coq mailing list

[Guillaume Dufay <Guillaume.Dufay AT sophia.inria.fr>]

Hello,

I'm having a weird problem with the strategie Cases.
Hereafter a small example in Coq :

Require Bool.

Definition is_true := true.

Definition foo := [b:bool]
  Cases b of
    is_true => true |
    _ => false
  end.

Print is_true.
Print foo.




And the result is :
> is_true = true
>     : bool 
> foo = [_:bool]true
>     : bool->bool

No pattern-matching is done on the redefined constructor true.
Is that a normal behaviour? Is there a way to avoid this?


Thank you in advance. Regards,


Guillaume Dufay