Skip to content

fix monPred scope binding

Ralf Jung requested to merge ralf/monpred-scope into master

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.

Edited by Ralf Jung

Merge request reports