git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/ElabTerm.hs
all commits
a2f90a5Better error message for impossible lambdas that don't pattern-matchDavid Raymond Christiansen 32f91a6Don't Force an implicit DelayEdwin Brady 95eee3cRemove no longer used primitives from TTEdwin Brady 8472966Remove Buffer/BitVectors from compiler/C rtsEdwin Brady c3f827fMake sure all patterns are top levelEdwin Brady 2d503f1Fix interactive proverEdwin Brady b5052ebNon-determining parameters not assumed injectiveEdwin Brady dbe0a3cCheck class arguments for injectivityEdwin Brady a281e23Class resolution should not use private instancesEdwin Brady f4aaf01Guard !! in forgetEnvEdwin Brady 84019b6Fix quasiquoted Raw binder termsDavid Raymond Christiansen 361efb5Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 147149bAdd 'determining parameters' for classesEdwin Brady 2a70296Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen be9ffc9Proper error message for missing eliminatorsEdwin Brady 5ce7362Type class resolution fixEdwin Brady 15ab5d5Better error message for qed in expressionsDavid Raymond Christiansen bb013f0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 426d052Add provenance flag to unification errorsEdwin Brady 8858c1aBasic handling of elaborator debugger invocationsDavid Raymond Christiansen c9b1759Fix type error in name reflectionDavid Raymond Christiansen a1c42adAdd "rewrite" to new-style tacticsDavid Raymond Christiansen 98c36eePush source locations around correctly for new-style tacticsDavid Raymond Christiansen 0222187Slightly more useful error messagesDavid Raymond Christiansen c726022Whitespace cleanupDavid Raymond Christiansen 1d64b2cFinalise terms before evaluation in new-style tacticsDavid Raymond Christiansen 1e488afAdd new-style tactics for getting source locationsDavid Raymond Christiansen 20e6028Merge branch 'master' into wip/tacticalDavid Raymond Christiansen ee8fce0Add "intro" tactic to new tacticsDavid Raymond Christiansen 7c9a1d0Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 8697358Fix scope error when shadowingEdwin Brady f327f18Raw quasiquote patternsDavid Raymond Christiansen 53cf150Check quasiquotation flag in elaborator on lhsEdwin Brady 2758aaeMerge branch 'wip/tactical' of https://github.com/david-christiansen/Idris-dev into david-christiansen-wip/tacticalEdwin Brady b048140Overloaded quasiquotationsDavid Raymond Christiansen c021042Quasiquotes for Raw termsDavid Raymond Christiansen 13e8ad8Plumb source locations through Tactical's elabDavid Raymond Christiansen 4d1759ePair syntax for unique typesEdwin Brady 2f96f33Split between primitive tactics and UIDavid Raymond Christiansen a0346b6Begin implementation of reflected elab monadDavid Raymond Christiansen 5f3e853Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 9330832Deal with unique types in 'do' betterEdwin Brady f17606a"claim" and "unfocus" tacticsDavid Raymond Christiansen 26cfbe9Scoped implicits fixEdwin Brady 39e4eb0IO primitives tweak to support JSEdwin Brady 3c187ceBetter tracking of FC in implicit coercions / DSLDavid Raymond Christiansen c729d2fSupport scoped type class constraintsEdwin Brady f6bcfb6Some tidying of scoped implicitsEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady