Jason Gross (Jan 12 2022 at 03:15): Jason Gross (Jan 12 2022 at 03:15):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...
Gaëtan Gilbert (Jan 12 2022 at 09:34):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?
Jason Gross (Jan 12 2022 at 20:50):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.
Jason Gross (Jan 24 2022 at 15:03):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: May 31 2023 at 16:01 UTC