Hi, I would like coq to stop printing specific notation in my goal. The notation lives in a certain scope. I would have expected that `Close Scope`

does this, but it behaves differently:

```
Close Scope nat_scope.
Goal ge 1 0.
```

Now it still prints

```
1 subgoal
========================= (1 / 1)
(1 >= 0)%nat
```

(I would like it to print just `ge 1 0`

, but keep other notation, so not use `Unset Printing Notations`

).

I'm on Coq 8.13.2, so unfortunately I don't have the `Disable Notation`

command yet. Is there another way to do this?

Try making a new notation to override the existing one `Notation ge := ge.`

To me this looks like a bug, but it is an old one, so there must be an explanation.

Meanwhile this works: `Disable Notation "_ >= _": nat_scope.`

After Close Scope, `(1 >= 0)%nat`

still parses, as intended, and you can also use closed scopes via at least Bind Scope, Arguments, and notations wrapping uses of %key. The "bug" is just to use the notations during pretty-printing as well.

Maybe you'd like pretty-printing to never use %, but using % seems a crucial feature when proving theory relating Nat, N and Z.

Yes the printing of ˋgeˋ with `<=`

is surprising.

Le lun. 31 juil. 2023 à 13:10, Zulip notifications <noreply@zulip.com> a

écrit :

Try `Close Scope nat_scope. Undelimit Scope nat_scope.`

(Note that if you `Unbind Scope nat_scope.`

or w/e, you'll lose the notation for numerals in your goal.)

Last updated: Jun 18 2024 at 20:02 UTC