Commit c8a06279 authored by Janno's avatar Janno

Don't `Declare Scope`.

parent 3e4cf901
......@@ -1166,7 +1166,6 @@ Implicit Types P Q R : PROP.
End setup.
End LetBindSetup.
Declare Scope HIDE.
Notation "'HIDDEN'" := (Envs _ _ _) : HIDE.
Delimit Scope HIDE with hide.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment