Commit b00ace04 authored by Ralf Jung's avatar Ralf Jung

Mark notation as "only printing"

Unfortunately, we currently have to keep the unicode-space hack in some places because Coq still complains about the notation otherwise
parent 1f8c4338
......@@ -7,22 +7,22 @@ Arguments Envs _ _%proof_scope _%proof_scope.
Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "​" := Enil (format "​") : proof_scope.
Notation H : P" := (Esnoc Γ H P)
Notation "​" := Enil (format "​", only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ H P)
(at level 1, P at level 200,
left associativity, format ​ H : P '//'") : proof_scope.
left associativity, format H : P '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'") :
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
Notation "Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Enil Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Δ '--------------------------------------' ∗ '//' Q '//'") : C_scope.
format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
Notation "Γ '--------------------------------------' □ Q" :=
(of_envs (Envs Γ Enil) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Q '//'") : C_scope.
format "Γ '--------------------------------------' □ '//' Q '//'", only printing) : C_scope.
Notation "​​ Q" := (of_envs (Envs Enil Enil) Q%I)
(at level 1, Q at level 200, format "​​ Q") : C_scope.
(at level 1, Q at level 200, format "​​ Q", only printing) : C_scope.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment