git.iko.soy/Idris-dev
on cb005bc help sign in
history ofsrc/Idris/Core/ProofState.hs
all commits
cb005bcFix overenthusiastic unificationEdwin Brady 39e4eb0IO primitives tweak to support JSEdwin Brady 72aa6b9Proper error when merging solutions failsEdwin Brady c729d2fSupport scoped type class constraintsEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady ba51147Removing matching on PSEdwin Brady 6d54cb3Disallow explicit types on LHSEdwin Brady 6b6aae0Avoid retrying unification problems constantlyEdwin Brady b0a0c0cImprovement for 'auto'Edwin Brady 127db00Lifted a FIXME from Core/ProofStateJan de Muijnck-Hughes 9fd9de7Proper error for missing eliminatorEdwin Brady 3ade599Partial evaluator fixesEdwin Brady 971d88dAnnotate several top-level functionsMichael Maloney 7e7368dStore kind in Pi bindersEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady a9dd2e4Lift out proof term into a separate moduleEdwin Brady e6e1ad9Unification fixEdwin Brady 0a1965eChange 'Not a guess' errorEdwin Brady 8ed343bRemove dodgy unification hackEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi 5045daeAdded tactic for case analysis. Also, induction now work on expressions instead of simply names.Ahmad Salim Al-Sibahi a0b05e2Allow induction on terms instead of simply namesAhmad Salim Al-Sibahi 921b766Fix name propagation in error messagesEdwin Brady 41f921fUnify more things!Edwin Brady d10c1e9Can't assume explicit names in updateSolvedEdwin Brady 5a5eecaMerge pull request #1143 from ahmadsalim/bug/inductionfixDavid Christiansen e36c883Fix #1015raichoo 78ff448Bug fixing of induction bugsAhmad Salim Al-Sibahi 62705e4Tweak mergeNotunifiedEdwin Brady f2bf55dMerge 'not unified' variablesEdwin Brady 51394aaAdd 'unify' tacticEdwin Brady 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