Looks like someone wrote Bind Scope monPred with bi. instead of Bind Scope bi_scope with monPred. and way later I added the Declare Scope to silence a Coq warning, and all the while nobody noticed until @Blaisorblade recently pointed this out.
Looks like someone wrote Bind Scope monPred with bi. instead of Bind Scope bi_scope with monPred. and way later I added the Declare Scope to silence a Coq warning, and all the while nobody noticed until @Blaisorblade recently pointed this out.