Imported Upstream version 8.6upstream/8.6

1 files changed, 6 insertions, 2 deletions

diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index ab6bf472..48fbe079 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -76,17 +76,21 @@ Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  & P  & Q }" (at level 0, x at level 99).
 
 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.
+Open Scope function_scope.
 Open Scope type_scope.
 
 (** ML Tactic Notations *)
 
 Declare ML Module "coretactics".
 Declare ML Module "extratactics".
-Declare ML Module "eauto".
+Declare ML Module "g_auto".
 Declare ML Module "g_class".
 Declare ML Module "g_eqdecide".
 Declare ML Module "g_rewrite".
-Declare ML Module "tauto".