@@ -430,15 +430,7 @@ elab ist info emode opts fn tm
430430 pimp (sMN 0 "P") Placeholder True,
431431 pexp l, pexp r])
432432 elab' ina fc (PAlternative (ExactlyOne delayok) as)
433− = do hnf_compute
434− ty <- goal
435− ctxt <- get_context
436− let (tc, _) = unApply ty
437− env <- get_env
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") $
433+ = do as' <- doPrune as
442434 (h : hs) <- get_holes
443435 case as' of
444436 [x] -> elab' ina fc x
@@ -449,14 +441,28 @@ elab ist info emode opts fn tm
449441 (map showHd as')))
450442 (do movelast h
451443 delayElab 5 $ do
452− focus h
453− tryAll (zip (map (elab' ina fc) as')
454− (map showHd as')))
444+ hs <- get_holes
445+ when (not (null hs)) $ do
446+ focus h
447+ as'' <- doPrune as'
448+ case as'' of
449+ [x] -> elab' ina fc x
450+ _ -> tryAll (zip (map (elab' ina fc) as'')
451+ (map showHd as'')))
455452 where showHd (PApp _ (PRef _ n) _) = n
456453 showHd (PRef _ n) = n
457454 showHd (PApp _ h _) = showHd h
458455 showHd x = NErased -- We probably should do something better than this here
459456
457+ doPrune as =
458+ do hnf_compute
459+ ty <- goal
460+ ctxt <- get_context
461+ let (tc, _) = unApply ty
462+ env <- get_env
463+ return $ pruneByType (map fst env) tc ctxt as
464+
465+
460466 isAmbiguous (CantResolveAlts _) = delayok
461467 isAmbiguous (Elaborating _ _ e) = isAmbiguous e
462468 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e