@@ -1076,11 +1076,15 @@ elab ist info emode opts fn tm
10761076 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
10771077 elab' ina fc (PQuoteName n) =
10781078 do ctxt <- get_context
1079− case lookupNameDef n ctxt of
1080− [(n', _)] -> do fill $ reflectName n'
1081− solve
1082− [] -> lift . tfail . NoSuchVariable $ n
1083− more -> lift . tfail . CantResolveAlts $ map fst more
1079+ env <- get_env
1080+ case lookup n env of
1081+ Just _ -> do fill $ reflectName n ; solve
1082+ Nothing ->
1083+ case lookupNameDef n ctxt of
1084+ [(n', _)] -> do fill $ reflectName n'
1085+ solve
1086+ [] -> lift . tfail . NoSuchVariable $ n
1087+ more -> lift . tfail . CantResolveAlts $ map fst more
10841088 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
10851089 elab' ina fc (PHidden t)
10861090 | reflection = elab' ina fc t