The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 04/03/2016 17:26, Jonathan Leivent wrote:
> Note that this works:
> 
> Definition my_struct : mixin_of cT :=
> let x := cT in
>   match x return (mixin_of x) with
>   | Pack _ c => c
>   end.
> 
> although that might just add to the mystery.

All right, I got it. This has nothing to do with the Variable outside
section stuff. This is just because of the meaning of pattern-matching
over variables as in De Bruijn variables vs. things that look like one
(including Definitions, Variables and the like).

This is the expected behaviour, although a bit puzzling at first. See
this bug report:

https://coq.inria.fr/bugs/show_bug.cgi?id=4405

Cheers,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature