git.iko.soy/Idris-dev
on 0cb9b4e help sign in
history ofsrc/Idris/Core/ProofState.hs
all commits
310f046Fix case split/unification bugEdwin Brady 3d2fa6cBetter elaboration of applicationsEdwin Brady 83f0af1Display expected type of RHS in error messagesEdwin Brady d5b66a9Show source location of case block namesDavid Raymond Christiansen 3b9206bError message instead of crash when searching on a guessDavid Raymond Christiansen ce403f6Merge remote-tracking branch 'upstream/master' into wip/tacticalDavid Raymond Christiansen 0497655Properly compute default lambda var namesDavid Raymond Christiansen 93dafdeMake sure deferred names are uniqueEdwin Brady c931effProof search improvementsEdwin Brady b1ce3cbImplement a form of pattern unificationEdwin Brady b573bf0Improve addImpl under PHiddenEdwin Brady 2e170bfRemove dubious matching ruleEdwin Brady 7bde028Use subst for intro, rather than updsubstDavid Raymond Christiansen 7095d6cProof search should only use user visible namesEdwin Brady 0e7c076Normalise types before detecting parametric argsEdwin Brady 01c911eFix missing case in `casetac`Brian Koropoff 268459cFailing 'focus' should be harmlessEdwin Brady 3034fb6Remove argument ordering hack in elaboratorEdwin Brady d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen 8ab2814Mark 'complete' terms to save time in elaborationEdwin Brady f987aecAdd info field to AppEdwin Brady 147149bAdd 'determining parameters' for classesEdwin Brady c66df51Propagate unification solutions into types on 'P'Edwin Brady be9ffc9Proper error message for missing eliminatorsEdwin Brady 6d768bbMore information if a function is overappliedEdwin Brady 01c4f2aA bit more unification error provenanceEdwin Brady 179c704Record provenance of types in 'fill' errorsEdwin Brady 426d052Add provenance flag to unification errorsEdwin Brady f17606a"claim" and "unfocus" tacticsDavid Raymond Christiansen 26cfbe9Scoped implicits fixEdwin Brady 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