如何暂时禁用 Coq 中的符号

当您熟悉项目时，符号很方便，但当您刚刚开始使用代码库时，符号可能会令人困惑。我知道你可以用白话关闭所有符号Set Printing All。但是，我想保留一些打印，例如隐式参数。全部打印如下：

Require Import Utf8_core. 
Set Printing All.
Theorem contradiction_implies_anything : forall P Q : Prop,
  (P /\ ~P) -> Q.
Proof.

给出以下证明状态：

1 subgoal (ID 120)

  ============================
  forall (P Q : Prop) (_ : and P (not P)), Q

差不多就这样了，但我想要_被删除和forall to be ∀然后展开我的笔记。

I tried Set Printing Notations如中所示Coq 参考手册 https://coq.inria.fr/refman/language/gallina-extensions.html#coq:flag.printing-all但这没有做任何事情，也没有启用

Set Printing Implicit.
Set Printing Coercions.
Set Printing Synth.
Set Printing Projections.

有趣的是Printing Notations你实际上必须Unset it.

Unset Printing Notations.

这是手册提示的地方 https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:flag.printing-notations:

Printing Notations:
控制是否尽可能使用符号来打印术语。默认开启。