20070607-0

When the same operator is imported from two different modules, there is a somewhat weird error:

open import Category
open import Setoid

...

f : (SlObj.arr f') o h == (SlObj.arr f)

gives

Don't know how to parse ((SlObj.arr f') o h) == (SlObj.arr f).
Could mean any one of:
  ((SlObj.arr f') o h) == (SlObj.arr f)
  ((SlObj.arr f') o h) == (SlObj.arr f)
when scope checking ((SlObj.arr f') o h) == (SlObj.arr f)

A better error message would be

Don't know how to parse ((SlObj.arr f') o h) == (SlObj.arr f).
Could mean any one of:
  Category._==_ ((SlObj.arr f') o h) (SlObj.arr f)
  Setoid._==_   ((SlObj.arr f') o h) (SlObj.arr f)
when scope checking ((SlObj.arr f') o h) == (SlObj.arr f)