The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

ldou AT cs.ecnu.edu.cn
 wrote:
>
> the result turns out to be:
> exists o' : o, (if o_dec o' ((e0 :: nil) :: nil) then true else false)
> = true
> but it should be :
> exists o' : o, (if o_dec o' ((("e0" :: nil) :: nil) ::nil) then true
> else false) = true
> Why is that?
>

Can you explain why you expected a different result? This looks correct
to me. Why would you expect an arbitrary [Diag] to be known to contain a
particular constant string?