如何在Coq中暂时禁用符号

Question

当您熟悉项目时，符号很方便，但是当您刚开始使用代码库时，可能会造成混淆。我知道您可以使用白话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设为∀，然后展开我的符号。

我按照Set Printing Notations的指示尝试了Coq Reference Manual，但是它什么也没做，也没有启用

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

Answer 1

Printing Notations的有趣之处在于您实际上必须Unset。

Unset Printing Notations.

Here's where the manual hints at it：

Printing Notations：控制是否在可能的情况下在打印术语中使用符号。 默认为开。