The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/22/2016 02:44 PM, Jonathan Leivent wrote:
> In this particular case, I did manage to use coercions.  I did have to 
> change a few tactics to accommodate the appearance of the coercion 
> function, but it worked.  It does feel a bit fragile, though.  In 
> particular, the user type that I want numerals to work for is also 
> declared to be a ring, and I need ring-simplify to work properly even 
> in other cases I haven't tried yet.  Maybe I can rig the Add Ring 
> declaration with the necessary preprocess/postprocess tactics to 
> unfold/fold the coercion function?
>
> But, I would like to avoid this by having everything handled in the 
> parse/print layers.

Another issue:  with the coercions in place, some proofs are much 
slower.  I don't know what is causing the slowdown.  Of course, one 
suspect would be that the coercion function - being in the actual terms 
as opposed to merely being something called and desugared by the parser 
- is somehow messing with my tactics.

-- Jonathan