Search code examples
coqcoercion

Is it possible to remove/override an existing coercion?

I have imported a Coq module which defines a coercion, but it does not fit my needs. Is there any way to remove or (locally) override it?

To be specific, say the module I imported defines a coercion

Coercion bool_to_nat (b:bool) := match b with true => 1 | false => 0 end.

but I want to use the opposite in my code

Local Coercion bool_to_nat' (b:bool) := match b with true => 0 | false => 1 end.

Coq gives a warning Ambiguous paths: [bool_to_nat'] : bool >-> nat and simply ignores my definition (can be checked by Goal false + 1 = true. reflexivity. Qed. Is it possible to convince Coq to respect my choice, at least locally in this file?

It would be a plus to be able to explicitly manipulate coercions after they are declared, like how one is able to manipulate hint databases. Are there such commands?

Solution

  • With Coq 8.15 you can import everything except coercions:

    Import -(coercions) ModuleName.

    Cf. the manual for import categories.