on 385dcbf help sign in
all commits
7a8217aUse Set for boundNamesInEdwin Brady c3def79Rename Tactical to ElabDavid Raymond Christiansen 7d02904Progress towards defining functions in TacticalDavid Raymond Christiansen da8b88ashow incomplete term holes for listy constructorsJP Smith 5d269e3:exec can take an expression as an argumentEdwin Brady 5804426Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 9c13628Merge branch 'master' into agda-style-recordssualitu 26dba59Mergesualitu 0269d05More record stuff.Sune Alkaersig 0f86748Fix build errors with GHC 7.10.1. Fixes #2080Jan Stolarek 13a36a3Annotate functions as %hint for auto searchEdwin Brady fc02362Support externally defined primitivesEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady bbbe880Merged.Sune Alkærsig 9596463Merge branch 'master' into agda-style-recordsSune Alkærsig f36a8f7Revamped record elaboration.Sune Alkærsig 174395bMerge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 15737d9Trickiness with implicits in dependent classesEdwin Brady aa33865Merge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 1bf2731issue #2004 resolved by --consolewith cmd line paramAndreas Reuleaux 6d188c4Begin to use a sum type for post-elab IState tweaksDavid Raymond Christiansen 361efb5Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 147149bAdd 'determining parameters' for classesEdwin Brady c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen 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 aca1148Merge branch 'master' into agda-style-recordstdidriksen 6fe15eaAllow type providers to have docstringsAdam Sandberg Eriksson 7ba4da0Instance docs: instance parameter documentationAdam Sandberg Eriksson 5ca59efInstance docs: haddocks grammarAdam Sandberg Eriksson 2d205a6Instance docs: basic plumbing of types and parsingAdam Sandberg Eriksson d4371e6Generate interface files for C->Idris callsEdwin Brady f7648dbForeign export lists in IOEdwin Brady 83793a6Add the ability for IDEs to get documentation overviewsDavid Raymond Christiansen 4d16a95Changed desugaring behavior to use <*> instead of <$>Tenor Biel 681d876Merge branch 'master' into agda-style-recordsSune Alkærsig 2758aaeMerge branch 'wip/tactical' of https://github.com/david-christiansen/Idris-dev into david-christiansen-wip/tacticalEdwin Brady 13e8ad8Plumb source locations through Tactical's elabDavid Raymond Christiansen 4d1759ePair syntax for unique typesEdwin Brady 173703dAdded new (co)record syntax.Sune Alkærsig a0346b6Begin implementation of reflected elab monadDavid Raymond Christiansen f17606a"claim" and "unfocus" tacticsDavid Raymond Christiansen 40d094dExpose equality proofs in with ruleEdwin Brady c918f44Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 26cfbe9Scoped implicits fixEdwin Brady b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen a87f69eMerge pull request #1885 from david-christiansen/issue/1860David Christiansen 914d992Bound the depth of hole searchingDavid Raymond Christiansen b8abab8Always show holes when pretty-printing delaborationsDavid Raymond Christiansen