Is it possible to remove/override an existing coercion?

Question

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?

Kimbell

I think it is not possible at the moment. Perhaps you could open an issue about this? – Sclerodermatous

@AntonTrunov I opened an issue here: github.com/coq/coq/issues/9275 – Kimbell

Answer 1

With Coq 8.15 you can import everything except coercions:

Import -(coercions) ModuleName.

Cf. the manual for import categories.

Unsheathe