diff options
| author | Jason Gross | 2015-06-24 15:41:11 +0200 |
|---|---|---|
| committer | Jason Gross | 2015-08-14 02:49:31 -0400 |
| commit | 6aa58955515dff338ea85d59073dfc0d0c7648ab (patch) | |
| tree | ed472dbf020c22a3080bc5e13a398914875bca11 /theories | |
| parent | 297b0cb44bbe8ec7304ca635c566815167266d4a (diff) | |
Move type_scope into user space, fix some output logs
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Notations.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 50728136ba..ef6125e6fa 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -79,6 +79,7 @@ Delimit Scope type_scope with type. Delimit Scope function_scope with function. Delimit Scope core_scope with core. +Bind Scope type_scope with Sortclass. Bind Scope function_scope with Funclass. Open Scope core_scope. |