aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [ide] Dynamic printing width.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [ide] richpp clenaupGravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Debug feeder is not needed anymore.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove richpp from fake_ide.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [error] Move back fatal_error to toplevelGravatar Emilio Jesus Gallego Arias2017-03-21
* [feedback] Allow to remove feedback listeners.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove redundant white spacing pp construct.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Force well-formed boxes by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Force well-tagged docs by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Implement n-ary glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Make pp public to allow serialization.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [ide] ide_slave doesnt't need to capture stdoutGravatar Emilio Jesus Gallego Arias2017-03-21
* [ide] Use "log via feedback".Gravatar Emilio Jesus Gallego Arias2017-03-21
* Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
|\
* | trivial: fix commentGravatar Matej Kosik2017-03-21
| * [misc] Remove warnings about String.setGravatar Emilio Jesus Gallego Arias2017-03-20
* | Merge PR#479: [future] Remove unused parameter greedy.Gravatar Maxime Dénès2017-03-20
|\ \
* \ \ Merge PR#487: Add a forgotten (?) line to "theories/Logic/vo.itarget".Gravatar Maxime Dénès2017-03-19
|\ \ \
| * | | Add a forgotten (?) line to "theories/Logic/vo.itarget".Gravatar Matej Kosik2017-03-19
|/ / /
* | | Merge PR#428: Report missing tactic arguments in error messageGravatar Maxime Dénès2017-03-17
|\ \ \
* \ \ \ Merge PR#437: Improve unification debug trace.Gravatar Maxime Dénès2017-03-17
|\ \ \ \
* \ \ \ \ Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-03-17
|\ \ \ \ \
* \ \ \ \ \ Merge PR#442: Allow interactive editing of Coq.Init.LogicGravatar Maxime Dénès2017-03-17
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#451: Add η principles for sigma typesGravatar Maxime Dénès2017-03-17
|\ \ \ \ \ \ \
* | | | | | | | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
* | | | | | | | Merge PR#267: Proposal for an update of the recommended style in programming ...Gravatar Maxime Dénès2017-03-15
|\ \ \ \ \ \ \ \
| | | | | | | | * [safe-string] Enable -safe-string !Gravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe-string] toolsGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe-string] ideGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe-string] plugins/extractionGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe-string] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe_string] toplevel/vernacGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe_string] toplevel/coqloopGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe-string] parsing/cLexerGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe_string] interp/dumpglobGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe_string] library/nameopsGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe_string] kernel/cemitcodesGravatar Emilio Jesus Gallego Arias2017-03-14
* | | | | | | | | Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoGravatar Maxime Dénès2017-03-14
|\ \ \ \ \ \ \ \ \
| | | | | | | * | | Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
| |_|_|_|_|_|/ / / |/| | | | | | | |
| | | | | | | | * [safe-string] kernel/nativevaluesGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe_string] kernel/term_typingGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe-string] lib/miscelaneaGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | * [safe-string] lib/cUnixGravatar Emilio Jesus Gallego Arias2017-03-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 22:54:49 +0000