aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
* 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
| | | | | | | | This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
* | Revert "So as to beautify to work, do not use notations in Inductive types"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98.
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
* | Revert "Temporary deactivate re-interpretation of terms in beautify."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81.
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
* | Revert "Fixing printing of pat%constr."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
* | Revert "Fixing printing of induction/destruct as."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 691dc7d88c6810333eecef7c2f0b8d8617d19ab1.
* | Revert "Fixing extra space in printing destruct/induction as."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907.
* | Revert "Fixing printing of inversion as."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 6da8866a4fd79029b22bd1bf7cde6725a9ea259c.
* | Revert "Fixing printing of keeping hyp on the fly."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit d408e09e5366899f4313f433cc9507ea92458c49.
* | Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c.
* | Revert "Protect printing of ltac's "context [...]" from possible collision"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd.
* | Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62.
* | Revert "Printing notations as parsed."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e.
* | Revert "Fixing printing of Arguments."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2.
* | Revert "Fixing printing of Polymorphic/Monomorphic."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933.
* | Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4.
* | Revert "Fixing printing of Instance."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217.
* | Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit e11620ce155529c0e577304427f9b05d38e73caf.
* | Revert "Fixing extra space in printing bullets."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc.
* | Revert "Removing unused generalization of pr_vernac over pr_constr and ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | pr_lconstr." This reverts commit ee882d4cf6e7d84dc4589535042bbefdec56a288.
* | Revert "Simplification in ppvernac.ml."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74.
* | Revert "Isolating and exporting a function for printing body of a recursive ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | definition." This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673.
* | Revert "Fixing printing of Register retroknowledge."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb.
* | Revert "Passing around the precedence to the generic printer so as to solve"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.
* | Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 90252e973f5bcafc5f3b0b18564612d7fb4503a8.
* | Revert "Taking into account the original grammar rule to print generic"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90.
* | Revert "Fixing extra space in front of terminal in printing vernac."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
* | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
* | Fixing extra space in front of terminal in printing vernac.Gravatar Hugo Herbelin2016-04-27
| | | | | | | | fix au revert [||]
* | Taking into account the original grammar rule to print genericGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | arguments of vernac extensions, so that in list with a separator, the separator is printed.
* | Temporary hack to restore missing printing of "constr:" in right-handGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | side of Ltac's "let ... in ..." or "match ... with ... => ... end". Example: Ltac f x := let x := 0 in constr:(S x). Print Ltac f. has a missing "constr:". Note: for generic arguments: "ltac:" is always used, even if a constr, etc.
* | Passing around the precedence to the generic printer so as to solveGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | the remaining issue with the fix to #3709. However, this does not solve the problem in mind which is that "intuition idtac; idtac" is printed with extra parentheses into "intuition (idtac; idtac)". If one change the level of printing of TacArg of Tacexp from latom to inherited, this breaks elsewhere, with "let x := (simpl) in idtac" printed "let x := simpl in idtac".
* | 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
| |
* | Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-04-27
| |
* | Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-04-27
| | | | | | | | No other changes (long only because of a change of indentation).
* | Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-04-27
| |
* | Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-04-27
| | | | | | | | Fixing : in Declare Module.
* | Fixing printing of Instance.Gravatar Hugo Herbelin2016-04-27
| |
* | Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-04-27
| |
* | Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-04-27
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 04:55:24 +0000