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.

Adding `(only parsing)`

at the end of the `Local Notation`

commands?

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

Mukesh Tiwari has marked this topic as resolved.

FWIW, to disable all notations you want `Set Printing Notations`

, or `Unset Printing All`

if you want to disable even more sugar

Last updated: Jun 25 2024 at 17:02 UTC