aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
...
* | | Revert "Fixing printing of keeping hyp on the fly."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Gravatar Hugo Herbelin2016-04-27
* | | Revert "Protect printing of ltac's "context [...]" from possible collision"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Printing notations as parsed."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of Arguments."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of Polymorphic/Monomorphic."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of Instance."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing extra space in printing bullets."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...Gravatar Hugo Herbelin2016-04-27
* | | Revert "Simplification in ppvernac.ml."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Isolating and exporting a function for printing body of a recursive d...Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of Register retroknowledge."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Passing around the precedence to the generic printer so as to solve"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Taking into account the original grammar rule to print generic"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing extra space in front of terminal in printing vernac."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Gravatar Hugo Herbelin2016-04-27
* | | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | | Fixing extra space in front of terminal in printing vernac.Gravatar Hugo Herbelin2016-04-27
* | | Taking into account the original grammar rule to print genericGravatar Hugo Herbelin2016-04-27
* | | Temporary hack to restore missing printing of "constr:" in right-handGravatar Hugo Herbelin2016-04-27
* | | Passing around the precedence to the generic printer so as to solveGravatar Hugo Herbelin2016-04-27
* | | Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-04-27
* | | Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-04-27
* | | Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-04-27
* | | Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-04-27
* | | Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-04-27
* | | Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of Instance.Gravatar Hugo Herbelin2016-04-27
* | | Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of Arguments.Gravatar Hugo Herbelin2016-04-27
* | | Printing notations as parsed.Gravatar Hugo Herbelin2016-04-27
* | | Revert "Protect printing of intro-patterns from collision when "[|" orGravatar Hugo Herbelin2016-04-27
* | | Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-04-27
* | | Protect printing of intro-patterns from collision when "[|" or "|]"Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of inversion as.Gravatar Hugo Herbelin2016-04-27
* | | Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-04-27
* | | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
* | | Temporary deactivate re-interpretation of terms in beautify.Gravatar Hugo Herbelin2016-04-27
* | | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* | | So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-04-27
* | | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
* | | Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27