Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | | | | | | Simplify some proofs using ring and field. | 2017-03-22 | ||
| * | | | | | | | | | Remove duplicate lemmas. | 2017-03-22 | ||
|/ / / / / / / / / | ||||
| | | | | * / / / | funind: Ignore missing info for current function | 2017-03-22 | ||
| | | |_|/ / / / | | |/| | | | | | ||||
* | | | | | | | | Merge branch 'v8.6' | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ | | |/ / / / / / | |/| | | | | | | ||||
* | | | | | | | | Merge PR#390: Updates to the Pretty Printing Infrastructure | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#478: Small optimization on handling of library state. | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR#482: [toplevel] Remove unusable option -notop | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | Add a few comments in term_typing.ml. | 2017-03-21 | ||
| | | | | | | * | | | | Do not typecheck twice the type of opaque constants. | 2017-03-21 | ||
| | | | | |_|/ / / / | | | | |/| | | | | | ||||
| | | * | | | | | | | [ide protocol] Add comment about leftover parameter. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Hide the internal representation of `std_ppcmds`. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Fix bug in richpp Format use. | 2017-03-21 | ||
| | | * | | | | | | | [extraction] Flush formatters at end of output. | 2017-03-21 | ||
| | | * | | | | | | | [xml] Restore protocol compatibility with 8.6. | 2017-03-21 | ||
| | | * | | | | | | | [stm] Add common toploop for workers. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Remove uses of expensive string_of_ppcmds. | 2017-03-21 | ||
| | | * | | | | | | | [pp] [ide] Minor cleanups in pp code. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Move terminal-specific tagging to the toplevel. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Remove special tag type and handler from Pp. | 2017-03-21 | ||
| | | * | | | | | | | [ide] Dynamic printing width. | 2017-03-21 | ||
| | | * | | | | | | | [ide] richpp clenaup | 2017-03-21 | ||
| | | * | | | | | | | [pp] Debug feeder is not needed anymore. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Remove richpp from fake_ide. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Make feedback the only logging mechanism. | 2017-03-21 | ||
| | | * | | | | | | | [error] Move back fatal_error to toplevel | 2017-03-21 | ||
| | | * | | | | | | | [feedback] Allow to remove feedback listeners. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Remove redundant white spacing pp construct. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Force well-formed boxes by construction. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Force well-tagged docs by construction. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Implement n-ary glue. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Make pp public to allow serialization. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Prepare for serialization, remove opaque glue. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Remove `Pp.stras`. | 2017-03-21 | ||
| | | * | | | | | | | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list` | 2017-03-21 | ||
| | | * | | | | | | | [pp] Remove unused printing tagging infrastructure. | 2017-03-21 | ||
| | | * | | | | | | | [ide] ide_slave doesnt't need to capture stdout | 2017-03-21 | ||
| | | * | | | | | | | [ide] Use "log via feedback". | 2017-03-21 | ||
| |_|/ / / / / / / |/| | | | | | | | | ||||
| | | | * | | | | | [safe-string] update dev/doc/changes | 2017-03-21 | ||
| |_|_|/ / / / / |/| | | | | | | | ||||
* | | | | | | | | Merge PR#134: Enable `-safe-string` | 2017-03-21 | ||
|\ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | trivial: fix comment | 2017-03-21 | ||
| | | | * | | | | | Merge PR#430: make `emit' tail recursive | 2017-03-20 | ||
| | | | |\ \ \ \ \ | ||||
| | | | | * | | | | | In the Kami project, that causes a stack overflow in one of the example files | 2017-03-20 | ||
| | | | |/ / / / / | ||||
| * | | | | | | | | [misc] Remove warnings about String.set | 2017-03-20 | ||
| | | | | | | * | | [future] Use eager evaluation for chaining values. | 2017-03-20 | ||
| | | | | |_|/ / | | | | |/| | | | ||||
* | | | | | | | | Merge PR#479: [future] Remove unused parameter greedy. | 2017-03-20 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#487: Add a forgotten (?) line to "theories/Logic/vo.itarget". | 2017-03-19 | ||
|\ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | Add a forgotten (?) line to "theories/Logic/vo.itarget". | 2017-03-19 | ||
|/ / / / / / / / / | ||||
| | | | | * | | | | Merge PR#429: Don't require printing-only notation to be productive | 2017-03-17 | ||
| | | | | |\ \ \ \ | ||||
* | | | | | \ \ \ \ | Merge PR#428: Report missing tactic arguments in error message | 2017-03-17 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#437: Improve unification debug trace. | 2017-03-17 | ||
|\ \ \ \ \ \ \ \ \ \ \ |