aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-22Mark ring morphisms as opaque.Guillaume Melquiond
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
2017-03-22[travis] [8.6.only] Backport latest changes from trunk.Emilio Jesus Gallego Arias
2017-03-22Make IZR use a compact representation of integers.Guillaume Melquiond
2017-03-22Fix broken evaluation strategies for ring and field.Guillaume Melquiond
2017-03-22Fix some typos.Guillaume Melquiond
2017-03-22Simplify some proofs using ring and field.Guillaume Melquiond
2017-03-22Remove duplicate lemmas.Guillaume Melquiond
2017-03-22funind: Ignore missing info for current functionTej Chajed
2017-03-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-03-22Merge PR#390: Updates to the Pretty Printing InfrastructureMaxime Dénès
2017-03-22Merge PR#478: Small optimization on handling of library state.Maxime Dénès
2017-03-22Merge PR#482: [toplevel] Remove unusable option -notopMaxime Dénès
2017-03-21Add a few comments in term_typing.ml.Maxime Dénès
2017-03-21Do not typecheck twice the type of opaque constants.Maxime Dénès
2017-03-21[ide protocol] Add comment about leftover parameter.Emilio Jesus Gallego Arias
2017-03-21[pp] Hide the internal representation of `std_ppcmds`.Emilio Jesus Gallego Arias
2017-03-21[pp] Fix bug in richpp Format use.Emilio Jesus Gallego Arias
2017-03-21[extraction] Flush formatters at end of output.Emilio Jesus Gallego Arias
2017-03-21[xml] Restore protocol compatibility with 8.6.Emilio Jesus Gallego Arias
2017-03-21[stm] Add common toploop for workers.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove uses of expensive string_of_ppcmds.Emilio Jesus Gallego Arias
2017-03-21[pp] [ide] Minor cleanups in pp code.Emilio Jesus Gallego Arias
2017-03-21[pp] Move terminal-specific tagging to the toplevel.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove special tag type and handler from Pp.Emilio Jesus Gallego Arias
2017-03-21[ide] Dynamic printing width.Emilio Jesus Gallego Arias
2017-03-21[ide] richpp clenaupEmilio Jesus Gallego Arias
2017-03-21[pp] Debug feeder is not needed anymore.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove richpp from fake_ide.Emilio Jesus Gallego Arias
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2017-03-21[error] Move back fatal_error to toplevelEmilio Jesus Gallego Arias
2017-03-21[feedback] Allow to remove feedback listeners.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove redundant white spacing pp construct.Emilio Jesus Gallego Arias
2017-03-21[pp] Force well-formed boxes by construction.Emilio Jesus Gallego Arias
2017-03-21[pp] Force well-tagged docs by construction.Emilio Jesus Gallego Arias
2017-03-21[pp] Implement n-ary glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Make pp public to allow serialization.Emilio Jesus Gallego Arias
2017-03-21[pp] Prepare for serialization, remove opaque glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove `Pp.stras`.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
2017-03-21[ide] ide_slave doesnt't need to capture stdoutEmilio Jesus Gallego Arias
2017-03-21[ide] Use "log via feedback".Emilio Jesus Gallego Arias
2017-03-21[safe-string] update dev/doc/changesEmilio Jesus Gallego Arias
2017-03-21Merge PR#134: Enable `-safe-string`Maxime Dénès
2017-03-21trivial: fix commentMatej Kosik
2017-03-20Merge PR#430: make `emit' tail recursiveMaxime Dénès
2017-03-20In the Kami project, that causes a stack overflow in one of the example filesPaul Steckler
2017-03-20[misc] Remove warnings about String.setEmilio Jesus Gallego Arias
2017-03-20[future] Use eager evaluation for chaining values.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-08 13:47:56 +0000