rocq-prover

How to temporarily disable notations in Coq


Notations are convenient when you're familiar with a project but can be confusing when you're just starting with a code base. I know you can turn off all notations with the vernacular Set Printing All. However, I want to keep some printing off, such as implicit arguments. Printing all as follows:

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

gives the following proof state:

1 subgoal (ID 120)

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

Which is almost there, but I would like the _ to be removed and the forall to be āˆ€ and just unfold my notations.

I tried Set Printing Notations as indicated in the Coq Reference Manual but that didn't do anything, nor did enabling

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

Solution

  • The funny thing about Printing Notations is that you actually have to Unset it.

    Unset Printing Notations.
    

    Here's where the manual hints at it:

    Printing Notations:
    Controls whether to use notations for printing terms wherever possible. Default is on.