@@ -430,15 +430,7 @@ elab ist info emode opts fn tm
430 pimp (sMN 0 "P") Placeholder True,
430 pimp (sMN 0 "P") Placeholder True,
431 pexp l, pexp r])
431 pexp l, pexp r])
432 elab' ina fc (PAlternative (ExactlyOne delayok) as)
432 elab' ina fc (PAlternative (ExactlyOne delayok) as)
433− = do hnf_compute
433+ = do as' <- doPrune as
436− let (tc, _) = unApply ty
438− let as' = pruneByType (map fst env) tc ctxt as
439−-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++
440−-- show (length as') ++ "\n" ++
441−-- showSep ", " (map showTmImpls as') ++ "\nEND") $
442 (h : hs) <- get_holes
434 (h : hs) <- get_holes
443 case as' of
435 case as' of
444 [x] -> elab' ina fc x
436 [x] -> elab' ina fc x
@@ -449,14 +441,28 @@ elab ist info emode opts fn tm
449 (map showHd as')))
441 (map showHd as')))
450 (do movelast h
442 (do movelast h
451 delayElab 5 $ do
443 delayElab 5 $ do
445+ when (not (null hs)) $ do
449+ [x] -> elab' ina fc x
453− tryAll (zip (map (elab' ina fc) as')
450+ _ -> tryAll (zip (map (elab' ina fc) as'')
454− (map showHd as')))
451+ (map showHd as'')))
455 where showHd (PApp _ (PRef _ n) _) = n
452 where showHd (PApp _ (PRef _ n) _) = n
456 showHd (PRef _ n) = n
453 showHd (PRef _ n) = n
457 showHd (PApp _ h _) = showHd h
454 showHd (PApp _ h _) = showHd h
458 showHd x = NErased -- We probably should do something better than this here
455 showHd x = NErased -- We probably should do something better than this here
461+ let (tc, _) = unApply ty
463+ return $ pruneByType (map fst env) tc ctxt as
460 isAmbiguous (CantResolveAlts _) = delayok
466 isAmbiguous (CantResolveAlts _) = delayok
461 isAmbiguous (Elaborating _ _ e) = isAmbiguous e
467 isAmbiguous (Elaborating _ _ e) = isAmbiguous e
462 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e
468 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e