aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#507: Intern names bound in match patternsMaxime Dénès
2017-03-23Intern names bound in match patternsTej Chajed
2017-03-23Merge PR#501: [travis] Fix iris-coq build.Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Maxime Dénès
2017-03-23Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#495: funind: Ignore missing info for current functionMaxime Dénès
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
2017-03-23Merge PR#491: Do not typecheck twice the type of opaque constants.Maxime Dénès
2017-03-22Merge PR#480: show unused intro pattern warningMaxime Dénès
2017-03-22Merge PR#493: [safe-string] update dev/doc/changesMaxime Dénès
2017-03-22Merge PR#415: Use a compact representation for real literalsMaxime Dénès
2017-03-22Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.Hugo Herbelin
2017-03-22[travis] Fix iris-coq build.Emilio Jesus Gallego Arias
2017-03-22Document the changes to IZR.Guillaume Melquiond
2017-03-22Make IZR a morphism for field.Guillaume Melquiond
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:15:41 +0000