aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2016-06-16Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-06-16Fixing printing of inversion as.Hugo Herbelin
2016-06-16Fixing extra space in printing destruct/induction as.Hugo Herbelin
2016-06-16Fixing printing of induction/destruct as.Hugo Herbelin
2016-06-16Fixing printing of pat%constr.Hugo Herbelin
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Merge remote-tracking branch 'github/pr/194' into trunkMaxime Dénès
2016-06-15Remove the syntax changes introduced by this branch.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-07printing.mllib: remove some other .mli-only from a .mllibPierre Letouzey
2016-06-07Adding an only printing flag to notations.Pierre-Marie Pédrot
2016-06-06Fixing problems introduced in 8.5 with Ltac trace report. E.g.Hugo Herbelin
2016-06-06About printing of traces of failures while calling ltac code.Hugo Herbelin
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-06-02Move ide serialization libraries from lib/ to ide/Emilio Jesus Gallego Arias
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-23 06:50:45 +0000