The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Edsko de Vries wrote:
> If we now do
>
>   Eval compute in g 0.
>
> we get
>
>      = match
>          match minus_n_n 0 in (_ = y) return (y = 0) with
>          | refl_equal => refl_equal 0
>          end in (_ = y) return (T y)
>        with
>        | refl_equal =>
>            match minus_n_n 0 in (_ = y) return (T y) with
>            | refl_equal => T0
>            end
>        end
>      : T 0
>
> whereas I'd much rather just get T0!

It looks like [minus_n_n] is set to be opaque, which means that the 
definitional equality may not expand [minus_n_n] to its definition, so 
no application of it can ever reduce to a [refl_equal] prof. You might 
be able to use the [Transparent] vernacular command, but that will fail 
if [minus_n_n] was originally defined opaquely. In that case, you'll 
need to redefine it transparently (end a definition with [Defined] 
instead of [Qed]). Alternatively, you can bring in an axiom and rewrite 
with [UIP_refl], a theorem you can get by importing [Eqdep] from the 
standard library.