on 50878fa help sign in
all commits
f1ff8fbMerge pull request #2634 from david-christiansen/namesInQQDavid Christiansen 92c1959Respect quotation when expanding parametersDavid Raymond Christiansen 6d7d3bdMerge pull request #2630 from david-christiansen/namesInQQDavid Christiansen 071d34bMake name operations on PTerm quotation-awareDavid Raymond Christiansen 49fae22Add option to desugar nats in REPL outputben-schulz 2f9d287Implicit fixEdwin Brady 4b3c477Merge pull request #2569 from GuglielmoS/fix/master/2241David Christiansen 0fbfeabImprove pruning of alternativesEdwin Brady 555feb5Add support to keep track of records in IStateGuglielmo Fachini b573bf0Improve addImpl under PHiddenEdwin Brady 7095d6cProof search should only use user visible namesEdwin Brady 740d82dDisplay normalised types on :t for expressionsEdwin Brady c9c3bfaSemantic highlighting of implicit fromIntegerDavid Raymond Christiansen bc2915cMerge remote-tracking branch 'upstream/master' into parser-highlightsDavid Raymond Christiansen 5da0d60Faster processing of alternativesEdwin Brady a54852bHighlighting for pairs, lists and sigmasDavid Raymond Christiansen 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen ac68541Dump highlighting infoDavid Raymond Christiansen 823be86Highlight postulates and their definitionsDavid Raymond Christiansen 202c913Logging levels must be explicitly mentioned.Jan de Muijnck-Hughes 63806e5Mark free implicits as dottedDavid Raymond Christiansen 6bf22eeMerge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 34f516dCanonicalize paths in internalappDavid Raymond Christiansen 9056a4aMerge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen bfacfbcBetter partial evaluation of polymorphic HOFsEdwin Brady cb1805bAdd local namespace access to ElabDavid Raymond Christiansen 727a3d6Fix transform elaborationEdwin Brady 1d474a2Merge remote-tracking branch 'refs/remotes/upstream/master' into issue/2333David Raymond Christiansen 5542d1cAdd maximum pretty-printer depth option.David Raymond Christiansen 3643346Fixed REPL for `:doc Type` to display documentation rather than an error messageRossMeikleham ec83cb2Fix Haddock parse errorDavid Raymond Christiansen 5a366acUnknown implicit checking for nullary functionsEdwin Brady 1054d7dAdd UnknownImplicit errorEdwin Brady fbdd59bMark instances on elaboration stackEdwin Brady 0819777Improved type-directed disambiguationEdwin Brady a7e434aAllow Elab scripts to register type class instancesDavid Raymond Christiansen 64ab360Tracking and highlighting of metavariablesDavid Raymond Christiansen 7e8e25bMerge branch 'master' into name-highlightsDavid Raymond Christiansen acdf90fBe a bit more conservative about highlighting outputDavid Raymond Christiansen 0419a12Highlight let bindingsDavid Raymond Christiansen 56b6850Precise highlighting of instancesDavid Raymond Christiansen cc83850Accurate highlighting for recordsDavid Raymond Christiansen 5cb8ec3Be more careful with implicit FCsDavid Raymond Christiansen 53e1281Remove PEqMelvar Chen 73b666bMerge remote-tracking branch 'refs/remotes/upstream/master' into name-highlightsDavid Raymond Christiansen 95d90f4Better highlighting for data declarationsDavid Raymond Christiansen 8984d49Remove PRefl and all references to itMelvar Chen 268296fHighlight the names in type declarationsDavid Raymond Christiansen 689e64bHighlight pi and lambda bindersDavid Raymond Christiansen c42673cHighlight pattern varsDavid Raymond Christiansen