git.iko.soy/Idris-dev
on master help sign in
Fix type error in name reflection
commitc9b1759d6167688b837a3d9469d952ecf8ffca0d authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 5 Mar 2015, 16:23 (12 years ago) parent29553b6
2 files changed+2−2
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Errors.idr+1−1 src/Idris/ElabTerm.hs+1−1
libs/prelude/Language/Reflection/Errors.idr+1−1
@@ -29,7 +29,7 @@ data Err = Msg String
2929 | NoTypeDecl TTName
3030 | NotInjective TT TT TT
3131 | CantResolve TT
32− | CantResolveAlts (List String)
32+ | CantResolveAlts (List TTName)
3333 | IncompleteTerm TT
3434 | UniverseError
3535 | ProgramLineComment
src/Idris/ElabTerm.hs+1−1
@@ -2600,7 +2600,7 @@ reflectErr (NotInjective t1 t2 t3) =
26002600reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
26012601reflectErr (CantResolveAlts ss) =
26022602 raw_apply (Var $ reflErrName "CantResolveAlts")
2603− [rawList (Var $ (sUN "String")) (map Var ss)]
2603+ [rawList (Var $ reflm "TTName") (map reflectName ss)]
26042604reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
26052605reflectErr UniverseError = Var $ reflErrName "UniverseError"
26062606reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"