aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Removing internal support for accepting "{struct x}" and co in "Theorem with".Gravatar Hugo Herbelin2017-04-09
* Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\
* | Fix higher-order pattern variables not being printed as "@?" (bug #5431).Gravatar Guillaume Melquiond2017-04-02
* | Merge PR#511: [stm] Remove some obsolete vernacs/classification.Gravatar Maxime Dénès2017-03-30
|\ \
* | | Do so that "About" tells if a reference is a coercion.Gravatar Hugo Herbelin2017-03-27
| * | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
|/ /
| * Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
| * Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Prepare for serialization, remove opaque glue.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
* Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
* Fixing Bug 5383 (Hyps Limit) + small refactoring.Gravatar Pierre Courtieu2017-03-07
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
| |\
| | * Fixing a little bug in printing cofix with no arguments.Gravatar Hugo Herbelin2017-01-05
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\| |
| * | Fixing printing of "ltac:" in tactics after surrounding parenthesesGravatar Hugo Herbelin2016-12-02
| * | Fixing printing of "Set Warnings Append".Gravatar Hugo Herbelin2016-12-02
| * | Fixing space in printing "Context".Gravatar Hugo Herbelin2016-12-02
| * | Fixing space in printing several list of implicit arguments.Gravatar Hugo Herbelin2016-12-02
| * | Fixing printing of "only parsing" in abbreviations.Gravatar Hugo Herbelin2016-12-02
| * | Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-12-02
| * | More on fixing #5098 (preserving printing of "in hyp").Gravatar Hugo Herbelin2016-12-02
| * | Properly parenthesize "ltac:" arguments (bug #5169).Gravatar Guillaume Melquiond2016-11-22
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| |
| * | Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| * | [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| * | Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \
| * | | Do not print dependent evars by default (expensive)Gravatar Matthieu Sozeau2016-11-05
| | * | Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| |/ /
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| |
| * | Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \
| | * | Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | |
| * | | Refine printing of pending unification constraintsGravatar Matthieu Sozeau2016-10-20
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\| | |
| * | | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
| |/ /
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
| * | Fixing a few confusions on the name of the beautify flag.Gravatar Hugo Herbelin2016-10-12
| * | Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
| * | Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | Fixing a beautifier bug pointed out by Emilio.Gravatar Hugo Herbelin2016-10-05
| * | Merge remote-tracking branch 'github/pr/305' into v8.6Gravatar Maxime Dénès2016-10-04
| |\ \
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| | |