aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* 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
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 06:37:52 +0000