aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
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
2016-04-27Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-04-27Fixing printing of inversion as.Hugo Herbelin
2016-04-27Fixing extra space in printing destruct/induction as.Hugo Herbelin
2016-04-27Fixing printing of induction/destruct as.Hugo Herbelin
2016-04-27Fixing printing of pat%constr.Hugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
2016-04-27Temporary deactivate re-interpretation of terms in beautify.Hugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-27So as to beautify to work, do not use notations in Inductive typesHugo Herbelin
2016-04-27A heuristic to add parentheses in the presence of rules such asHugo Herbelin
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-04-25Removing dead code related to printing of ML tactics in Pptactic.Pierre-Marie Pédrot
2016-04-19Revert "Fixing printing of surrounding parentheses in "ltac:"."Hugo Herbelin
2016-04-17Fixing printing of surrounding parentheses in "ltac:".Hugo Herbelin
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-12Fixing printing of "destruct in" after ce71ac17268f.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-23 08:00:24 +0000