git.iko.soy/Idris-dev
on dcdebfc help sign in
history ofsrc/Idris/Core/ProofState.hs
all commits
ff742feActually track applications in the elaborator wrt unification failsDavid Raymond Christiansen b38bc03Add basic elaboration context tracking to unificationDavid Raymond Christiansen d88d1caFixes idris-lang/Idris-dev#971. Renames induction holes such that they are unique in context.Ahmad Salim Al-Sibahi 88f88ebUnification tweak; better disambiguationEdwin Brady 1f897b1Fix for matchProblemsEdwin Brady ecfb293Evaluator bug fixEdwin Brady 6d3863dBetter environment management in unificationEdwin Brady 2cff556Another unification fixEdwin Brady c959fb0Unification changesEdwin Brady 41d3dafUse the pprint library to insert line breaksDavid Raymond Christiansen 13f3c29Basic functioning with new pretty-printerDavid Raymond Christiansen 1dfc8fdFix typo that led to unification bugEdwin Brady d82f5feMerge branch 'text-names'Edwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady a611debFix memory leakEdwin Brady dfc3e44Shave a bit more off IBC sizeEdwin Brady ba15257Another small reduction in calls to TT.(==)Edwin Brady f47329cShortcut unification updatesEdwin Brady 4e6adebSeparate Core NFData instancesEdwin Brady fa364caCheck for cyclic solutions in unificationEdwin Brady fef1207Make note of unapplied unifiation solutionsEdwin Brady 3191f16Induction works for all types with eliminators now (some eliminators still need fixing) including those with indicies.Ahmad Salim Al-Sibahi d7f4e11Induction now works on types with parametersAhmad Salim Al-Sibahi 0700c58Fix another INTERNAL ERROREdwin Brady 2f5c756Better error message for 'Not a guess'Edwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna