git.iko.soy/Idris-dev
on 1b71663 help sign in
history ofsrc/Idris/Core/ProofTerm.hs
all commits
3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice fb185aaCheck for linearity of constructorsEdwin Brady e3daf28Add RigCount to environmentEdwin Brady 2196023Fix patvar naming for implicitsEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0896073Added documentation for modules.Jan de Muijnck-Hughes 2e170bfRemove dubious matching ruleEdwin Brady 8ab2814Mark 'complete' terms to save time in elaborationEdwin Brady f987aecAdd info field to AppEdwin Brady 7a8217aUse Set for boundNamesInEdwin Brady c66df51Propagate unification solutions into types on 'P'Edwin Brady f17606a"claim" and "unfocus" tacticsDavid Raymond Christiansen 6b6aae0Avoid retrying unification problems constantlyEdwin Brady b0a0c0cImprovement for 'auto'Edwin Brady 971d88dAnnotate several top-level functionsMichael Maloney 788f800Record import paths in ibcEdwin Brady 42c694cMore efficiency improvementsEdwin Brady 2418336Save some allocations in updateSolvedEdwin Brady d6057b5Search subterm for goal firstEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady a9dd2e4Lift out proof term into a separate moduleEdwin Brady