Note a regressed error message

Author: grunweg

MathlibTest/DifferentialGeometry/Notation.lean

@@ -547,38 +547,33 @@ section error
 -- yields a parse error, "unexpected token '/--'; expected term"
 -- #check CMDiffAt[s] f
 
-/--
+-- TODO: the old error message here was better; somehow restore it!
+/-
 error: Type mismatch
   f
 has type
   M → M'
 of sort `Type (max u_10 u_4)` but is expected to have type
   WithTop ℕ∞
 of sort `Type`
----
+-/
+
+/--
 error: Expected
   m
 of type
   M
-to be a function
+to be a function, or to be coercible to a function
 -/
 #guard_msgs in
 #check CMDiffAt[s] f m
 
 /--
-error: Type mismatch
-  f
-has type
-  M → M'
-of sort `Type (max u_10 u_4)` but is expected to have type
-  WithTop ℕ∞
-of sort `Type`
----
 error: Expected
   m
 of type
   M
-to be a function
+to be a function, or to be coercible to a function
 -/
 #guard_msgs in
 #check CMDiffAt[s] f m