aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Printing notations as parsed.Gravatar Hugo Herbelin2016-06-16
* So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-06-16
* Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
* Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of inversion as.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* \ Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \
| | * Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \
* | | | printing.mllib: remove some other .mli-only from a .mllibGravatar Pierre Letouzey2016-06-07
| | * | Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
| |/ / |/| |
| * | Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
* | | About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
* | | Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | | Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | | Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | | Move ide serialization libraries from lib/ to ide/Gravatar Emilio Jesus Gallego Arias2016-06-02
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\| |
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
* | | Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Actually using the symbol information to print Tactic Notations properly.Gravatar Pierre-Marie Pédrot2016-05-08
* | | Removing dead code in Pptactic.Gravatar Pierre-Marie Pédrot2016-05-08
* | | Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
* | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | | Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* | | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* | | Revert "So as to beautify to work, do not use notations in Inductive types"Gravatar Hugo Herbelin2016-04-27
* | | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Temporary deactivate re-interpretation of terms in beautify."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of pat%constr."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of induction/destruct as."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing extra space in printing destruct/induction as."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of inversion as."Gravatar Hugo Herbelin2016-04-27
* | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 07:15:23 +0000