@@ -98,7 +98,10 @@ elab ist info pattern tm
9898 [pimp (MN 0 "a") t,
9999 pimp (MN 0 "P") Placeholder,
100100 pexp l, pexp r])
101− elab' (PAlternative as) = tryAll (zip (map elab' as) (map showHd as))
101+ elab' (PAlternative as)
102+ = let as' = pruneAlt as in
103+ try (tryAll (zip (map elab' as') (map showHd as')))
104+ (tryAll (zip (map elab' as) (map showHd as)))
102105 where showHd (PApp _ h _) = show h
103106 showHd x = show x
104107 elab' (PRef fc n) | pattern && not (inparamBlock n)
@@ -214,6 +217,19 @@ elab ist info pattern tm
214217 (elabArgs ((n,(lazy, t)):failed) r ns args)
215218 else do focus n; elabE t; elabArgs failed r ns args
216219
220+pruneAlt :: [PTerm] -> [PTerm]
221+pruneAlt xs = map prune xs
222+ where
223+ prune (PApp fc1 (PRef fc2 f) as)
224+ = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)
225+ prune t = t
226+
227+ choose f (PAlternative as) = PAlternative (filter (headIs f) as)
228+ choose f t = t
229+
230+ headIs f (PApp _ (PRef _ f') _) = f == f'
231+ headIs f _ = True -- keep if it's not an application
232+
217233trivial :: IState -> Elab ()
218234trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))
219235 (do env <- get_env