@@ -98,7 +98,10 @@ elab ist info pattern tm
98 [pimp (MN 0 "a") t,
98 [pimp (MN 0 "a") t,
99 pimp (MN 0 "P") Placeholder,
99 pimp (MN 0 "P") Placeholder,
100 pexp l, pexp r])
100 pexp l, pexp r])
101+ elab' (PAlternative as)
102+ = let as' = pruneAlt as in
103+ try (tryAll (zip (map elab' as') (map showHd as')))
101− elab' (PAlternative as) = tryAll (zip (map elab' as) (map showHd as))
104+ (tryAll (zip (map elab' as) (map showHd as)))
102 where showHd (PApp _ h _) = show h
105 where showHd (PApp _ h _) = show h
103 showHd x = show x
106 showHd x = show x
104 elab' (PRef fc n) | pattern && not (inparamBlock n)
107 elab' (PRef fc n) | pattern && not (inparamBlock n)
@@ -214,6 +217,19 @@ elab ist info pattern tm
214 (elabArgs ((n,(lazy, t)):failed) r ns args)
217 (elabArgs ((n,(lazy, t)):failed) r ns args)
215 else do focus n; elabE t; elabArgs failed r ns args
218 else do focus n; elabE t; elabArgs failed r ns args
220+pruneAlt :: [PTerm] -> [PTerm]
221+pruneAlt xs = map prune xs
223+ prune (PApp fc1 (PRef fc2 f) as)
224+ = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)
227+ choose f (PAlternative as) = PAlternative (filter (headIs f) as)
230+ headIs f (PApp _ (PRef _ f') _) = f == f'
231+ headIs f _ = True -- keep if it's not an application
217trivial :: IState -> Elab ()
233trivial :: IState -> Elab ()
218trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))
234trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))
219 (do env <- get_env
235 (do env <- get_env