The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Sun, Jun 16, 2013 at 7:00 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> You can only do a syntactic match when you're building a proof in Ltac, not
> within a gallina function.  Gallina (the non-Ltac Coq language) doesn't have
> any notion of syntactic equality, and you can't access the definitional
> equality.  As a rule of thumb, gallina functions need to respect equality;
> if substituting (propositional) equals for equals changes the behavior of
> the function, then you can't do it in Gallina.  You could try Mtac (I've
> never tried it), which, I think, does some tricks with delaying computation
> until you run the code.  But I don't think you can prove much about Mtac
> code.  Alternatively, you could reify the types you use so that you only
> consider a subset of Type with decidable equality.

I see the problem. Anyway, I've learned that my approach is
ill-adviced anyway. I'm going to change my strategy.

Thanks!

--
www.mhelvens.net