## Stream: Coq users

### Topic: ✔ Disabling Local Notation in a Coq file

#### Mukesh Tiwari (Jan 09 2023 at 05:39):

Hi everyone,

I am working with a Coq file with a lot of local notations and I find it hard to work with it when proving a lemma. Basically, during the proof, it shows the notation while I want to see the text part. Is there a way to do this? For example, the Coq file I am working roughly looks like this:

``````  Local Notation "x =S= y" := (eqSAP x y = true) (at level 70).
Local Notation "[P1]" := (uop_manger_phase_1 eqA addP).  (* Phase 1 reduction *)
Local Notation "[P2]" := (@uop_manger_phase_2 A P lteA). (* Phase 2 reduction *)

Lemma that I want to prove is:
Lemma P1_P2_commute : ∀ X, ([P2] ([P1] X)) =S= ([P1] ([P2] X)).
``````

I want to set some flags such that when I start proving the `P1_P2_commute`, it should look like :

``````  Lemma P1_P2_commute : ∀ X, ([P2] ([P1] X)) =S= ([P1] ([P2] X)).
Proof.
At this point, if I am looking at the Coq goal it should appear like:

∀ X : finite_set (A * P),
eqSAP (@uop_manger_phase_2 A P lteA (uop_manger_phase_1 eqA addP X))
(uop_manger_phase_1 eqA addP (@uop_manger_phase_2 A P lteA X)) = true.
``````

I have tried `Set Printing All`, suggested Stackoverflow, but it is not working for me.

#### Pierre Roux (Jan 09 2023 at 07:19):

Adding `(only parsing)` at the end of the `Local Notation` commands?

#### Mukesh Tiwari (Jan 09 2023 at 10:08):

Thank you very much @Pierre Roux ! This is what I was looking for.

#### Notification Bot (Jan 09 2023 at 10:08):

Mukesh Tiwari has marked this topic as resolved.

#### Paolo Giarrusso (Jan 09 2023 at 13:43):

FWIW, to disable all notations you want `Set Printing Notations`, or `Unset Printing All` if you want to disable even more sugar

Last updated: Oct 04 2023 at 18:01 UTC