@@ -413,14 +413,15 @@ elab ist info emode opts fn tm
413 pimp (sUN "B") Placeholder False,
413 pimp (sUN "B") Placeholder False,
414 pexp l, pexp r])
414 pexp l, pexp r])
415 elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)
415 elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)
416− = case t of
416+ = case p of
417− Placeholder ->
417+ IsType -> asType
418 do hnf_compute
420 do hnf_compute
419 g <- goal
421 g <- goal
420 case g of
422 case g of
421 TType _ -> asType
423 TType _ -> asType
422 _ -> asValue
424 _ -> asValue
424 where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy)
425 where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy)
426 pexp (PLam fc n nfc Placeholder r)])
427 pexp (PLam fc n nfc Placeholder r)])