aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-08Actually using the symbol information to print Tactic Notations properly.Pierre-Marie Pédrot
2016-05-08Removing dead code in Pptactic.Pierre-Marie Pédrot
2016-05-08Pass user symbol to tactic notation printers.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 07:34:05 +0000