aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
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
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-10Extruding the print_atom primitive.Pierre-Marie Pédrot
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Removing automatic printing of leading space in auto_using andHugo Herbelin
2016-04-09Simplifying code for printing VERNAC EXTEND.Hugo Herbelin
2016-04-09Fixing extra space in printing inductive types with no explicit type given.Hugo Herbelin
2016-04-09In pr_clauses, do not print a leading space by default so that it canHugo Herbelin
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-04-08Fixing printing of Tactic Notations with tactic arguments.Pierre-Marie Pédrot
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-04-04Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Matthieu Sozeau
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-25Univs: fix get_current_context (bug #4603, part I)Matthieu Sozeau
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Print Ltac to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-19Removing the untyped representation of genargs.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 13:39:01 +0000