With 8.8.2 the code below compiles successfuly, but from 8.9 it fails with “Error: No interpretation for string “a”.”:
Require String. Definition f (x : String.string) := tt. Arguments f _%string_scope. Check f "a".
I tried to modernize it, but could not get it to compile (without import String which messes with List.++)
Require String. Delimit Scope string_scope with lstring. Bind Scope string_scope with String.string. Definition f (x : String.string) := tt. (*Arguments f _%string_scope.*) Arguments f _%lstring. Check f "a".