@@ -51,7 +51,6 @@ import Data.Traversable (Traversable)
51import Data.Typeable
51import Data.Typeable
52import GHC.Generics (Generic)
52import GHC.Generics (Generic)
55data ElabWhat = ETypes | EDefns | EAll
54data ElabWhat = ETypes | EDefns | EAll
56 deriving (Show, Eq)
55 deriving (Show, Eq)
@@ -2279,25 +2278,41 @@ allNamesIn tm = nub $ ni 0 [] tm
2279 ni 0 env (PPatvar _ n) = [n]
2278 ni 0 env (PPatvar _ n) = [n]
2280 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2279 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2281 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2280 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2281+ ni 0 env (PWithApp _ f a) = ni 0 env f ++ ni 0 env a
2282+ ni 0 env (PAppImpl t _) = ni 0 env t
2282 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2283 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2283 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2284 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2284 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2285 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2285 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2286 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2286 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2287 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2287 ni 0 env (PHidden tm) = ni 0 env tm
2288 ni 0 env (PHidden tm) = ni 0 env tm
2289+ ni 0 env (PGoal _ t _ sc) = ni 0 env t ++ ni 0 env sc
2290+ ni 0 env (PIdiom _ tm) = ni 0 env tm
2288 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2291 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2289 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2292 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2290 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2293 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2291 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2294 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2292 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2295 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2293 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2296 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2297+ ni 0 env (PAs _ _ tm) = ni 0 env tm
2298+ -- Just take the first, when disambiguating, since the shape will be
2299+ -- the same and we'll get the name root
2300+ ni 0 env (PAlternative ns (ExactlyOne _) (a : as))
2301+ = map snd ns ++ ni 0 env a
2294 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2302 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2295 ni 0 env (PUnifyLog tm) = ni 0 env tm
2303 ni 0 env (PUnifyLog tm) = ni 0 env tm
2296 ni 0 env (PDisamb _ tm) = ni 0 env tm
2304 ni 0 env (PDisamb _ tm) = ni 0 env tm
2297 ni 0 env (PNoImplicits tm) = ni 0 env tm
2305 ni 0 env (PNoImplicits tm) = ni 0 env tm
2306+ ni 0 env (PCoerced tm) = ni 0 env tm
2307+ ni 0 env (PRunElab _ tm _) = ni 0 env tm
2308+ ni 0 env (PConstSugar _ tm) = ni 0 env tm
2309+ ni 0 env tm@(PDoBlock _) = concatMap (ni 0 env) (children tm)
2310+ ni 0 env tm@(PProof _) = concatMap (ni 0 env) (children tm)
2311+ ni 0 env tm@(PTactics _) = concatMap (ni 0 env) (children tm)
2299 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2313 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2300 ni i env (PUnquote tm) = ni (i - 1) env tm
2314 ni i env (PUnquote tm) = ni (i - 1) env tm
2301 ni i env tm = concatMap (ni i env) (children tm)
2316 ni i env tm = concatMap (ni i env) (children tm)
2303 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2318 niTacImp i env (TacImp _ _ scr _) = ni i env scr