Skip to content

GitLab

Commit fab93130 authored by Ralf Jung's avatar Ralf Jung
Browse files

get rid of the remaining empty-unicode-space hacks

parent 3b4865f8
Hide whitespace changes
Inline Side-by-side
theories/proofmode/notation.v
View file @ fab93130
...@@ -7,7 +7,7 @@ Arguments Envs _ _%proof_scope _%proof_scope. ...@@ -7,7 +7,7 @@ Arguments Envs _ _%proof_scope _%proof_scope.
Arguments Enil {_}. Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope. Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "​" := Enil (format "​", only printing) : proof_scope. Notation "" := Enil (format "", only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ H P) Notation "Γ H : P" := (Esnoc Γ H P)
(at level 1, P at level 200, (at level 1, P at level 200,
left associativity, format "Γ H : P '//'", only printing) : proof_scope. left associativity, format "Γ H : P '//'", only printing) : proof_scope.
......
Supports Markdown
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