Is there a way to deactivate the printing of evar instances? `Unset Printing Existential Instances`

worked in Coq 8.4, but since Coq 8.5 it seems to only impact the display of evars in the `with`

part of displaying existentials...

it's off by default

```
Goal nat -> exists x, x = 0.
intros n.
eexists.
(* goal: ?x = 0 *)
Set Printing Existential Instances.
(* goal: ?x@{n:=n} = 0 *)
```

What's the problem with that?

I want to disable the verbosity of things like:

```
Goal forall x y : nat, x = y -> exists n : nat, n = n.
intros; eexists.
subst.
(* ?n@{x:=y; y:=y} = ?n@{x:=y; y:=y} *)
```

I feel like Coq is right to display the long form here, since the variable assignment is ambiguous and the incorrect lambda-term might be created after unification. I suppose Coq could use a more compact notation to show that substituting `n`

with a term containing `y`

is a bad idea.

I agree that Coq is right to display it by default, but I want an option to disable it in cases where the substituted term is enormous and irrelevant to the proof I'm doing (for example because the evar is of type nat and the substituted variable is a proof of some non-singleton Prop)

Last updated: Oct 13 2024 at 01:02 UTC