walker (Apr 26 2023 at 07:36): walker (Apr 26 2023 at 07:36):So in mathcomp:
From mathcomp Require Import all_ssreflect.
Locate "\o".
(*Notation "f1 \o f2" := (comp f1 f2) : fun_scope (default interpretation)*)
But in a file called utils.v I have :
Notation " g ∘ f " := (comp g f) (at level 40, left associativity).
Now I want t force coq to disable that other notation from mathcomp so it does not appear in interactive proofs, how can i do that?
Ideally I would want to do it so that it is reflected on every file that imports mathcomp.
Pierre Roux (Apr 26 2023 at 08:07):You should probably look for Disable Notation in the manual (available since Coq 8.17).
walker (Apr 26 2023 at 08:22):thanks, unfortunately today is not the day I move to 8.17 because I am using mathcomp 2.0 and it didn't compile on 8.17, but thanks, I wll bookmark this for when I upgrade
Pierre Roux (Apr 26 2023 at 08:24):Just use the hierarchy-builder branch instead of the alpha mathcomp-2 tag, this currently supports Coq 8.16, 8.17 and master.
Last updated: Oct 13 2024 at 01:02 UTC