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