aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
2016-04-27Revert "So as to beautify to work, do not use notations in Inductive types"Hugo Herbelin
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27Revert "Temporary deactivate re-interpretation of terms in beautify."Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Revert "Fixing printing of pat%constr."Hugo Herbelin
2016-04-27Revert "Fixing printing of induction/destruct as."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing destruct/induction as."Hugo Herbelin
2016-04-27Revert "Fixing printing of inversion as."Hugo Herbelin
2016-04-27Revert "Fixing printing of keeping hyp on the fly."Hugo Herbelin
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Hugo Herbelin
2016-04-27Revert "Protect printing of ltac's "context [...]" from possible collision"Hugo Herbelin
2016-04-27Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Hugo Herbelin
2016-04-27Revert "Printing notations as parsed."Hugo Herbelin
2016-04-27Revert "Fixing printing of Arguments."Hugo Herbelin
2016-04-27Revert "Fixing printing of Polymorphic/Monomorphic."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Hugo Herbelin
2016-04-27Revert "Fixing printing of Instance."Hugo Herbelin
2016-04-27Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing bullets."Hugo Herbelin
2016-04-27Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...Hugo Herbelin
2016-04-27Revert "Simplification in ppvernac.ml."Hugo Herbelin
2016-04-27Revert "Isolating and exporting a function for printing body of a recursive d...Hugo Herbelin
2016-04-27Revert "Fixing printing of Register retroknowledge."Hugo Herbelin
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
2016-04-27Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Hugo Herbelin
2016-04-27Revert "Taking into account the original grammar rule to print generic"Hugo Herbelin
2016-04-27Revert "Fixing extra space in front of terminal in printing vernac."Hugo Herbelin
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Fixing extra space in front of terminal in printing vernac.Hugo Herbelin
2016-04-27Taking into account the original grammar rule to print genericHugo Herbelin
2016-04-27Temporary hack to restore missing printing of "constr:" in right-handHugo Herbelin
2016-04-27Passing around the precedence to the generic printer so as to solveHugo Herbelin
2016-04-27Fixing printing of Register retroknowledge.Hugo Herbelin
2016-04-27Isolating and exporting a function for printing body of a recursive definition.Hugo Herbelin
2016-04-27Simplification in ppvernac.ml.Hugo Herbelin
2016-04-27Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
2016-04-27Fixing extra space in printing bullets.Hugo Herbelin
2016-04-27Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
2016-04-27Fixing printing of Instance.Hugo Herbelin
2016-04-27Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-04-27Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-04-27Fixing printing of Arguments.Hugo Herbelin
2016-04-27Printing notations as parsed.Hugo Herbelin
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" orHugo Herbelin
2016-04-27Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
2016-04-27Protect printing of intro-patterns from collision when "[|" or "|]"Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 02:14:38 +0000