git.iko.soy/Idris-dev
on 54e4e41 help sign in
history ofsrc/Idris/Core/TT.hs
all commits
64df5f6Added WHNF moduleEdwin Brady 212587bRemove 'score' and guesswork from error messagesEdwin Brady e1c79efBetter error when no alternative is validEdwin Brady 5da0d60Faster processing of alternativesEdwin Brady 5fb7ff3Add export list to TTNiklas Larsson ec0b043Parser-driven highlighting of quasiquoted regionsDavid Raymond Christiansen 520f367Initial parser-driven highlightingDavid Raymond Christiansen 8d96041Annotate links with their URLDavid Raymond Christiansen e9e7993Replace absurd syntax rule FCsDavid Raymond Christiansen bf6dbf9Fix for GHC 7.10David Raymond Christiansen 5542d1cAdd maximum pretty-printer depth option.David Raymond Christiansen 4ede52dAllow the pretty-printing of Raw termsDavid Raymond Christiansen 1054d7dAdd UnknownImplicit errorEdwin Brady 2c609aeEnvironment fix in prepare_applyEdwin Brady e6e5472Fix a few user-visible leftover uses of “Float”Melvar Chen 8f9901dAnnotate module imports in source codeDavid Raymond Christiansen 77a732eAdd workaround for partial FC functionsDavid Raymond Christiansen 95d90f4Better highlighting for data declarationsDavid Raymond Christiansen 924f791Highlighting for infix operatorsDavid Raymond Christiansen 4ebafb4Highlight names of simple variable referencesDavid Raymond Christiansen c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen 8073344Better errors on stuck reflected elaboratorsDavid Raymond Christiansen 8ab1ac6Richer universe error objectsDavid Raymond Christiansen d1941f5Fix bug with Type*/AnyType in data declsEdwin Brady 3592edbReflection for SN, plus an SN for meta-stuffDavid Raymond Christiansen d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen 370939bMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady f987aecAdd info field to AppEdwin Brady f1c6e39Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 187730aAdd missing clause in showCGSam Elliott 5804426Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 95eee3cRemove no longer used primitives from TTEdwin Brady 8472966Remove Buffer/BitVectors from compiler/C rtsEdwin Brady 2d503f1Fix interactive proverEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady dbe0a3cCheck class arguments for injectivityEdwin Brady f4aaf01Guard !! in forgetEnvEdwin Brady d36f582Move comment about error reflection back homeDavid Raymond Christiansen 2a70296Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen c66df51Propagate unification solutions into types on 'P'Edwin Brady be9ffc9Proper error message for missing eliminatorsEdwin Brady 5ce7362Type class resolution fixEdwin Brady 6d768bbMore information if a function is overappliedEdwin Brady 01c4f2aA bit more unification error provenanceEdwin Brady 75f6c2dAdd :core to the REPLDavid Raymond Christiansen bb013f0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 3d87454TT pretty-printing - also in elab debugDavid Raymond Christiansen 179c704Record provenance of types in 'fill' errorsEdwin Brady 426d052Add provenance flag to unification errorsEdwin Brady