Issue721a.agda

-- 2012-10-20 Andreas
module Issue721a where

data Bool : Set where
  false true : Bool

record Foo (b : Bool) : Set where
  field
    _*_ : Bool → Bool → Bool

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

test : (F : Foo false) (x : Bool) → let open Foo F in _*_ x ≡ (λ x → x)
test F x = x
-- Don't want to see .Issue632._.* in the error message