Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Put the "cofix" tactic in the monad. | 2016-05-16 | |
| | |||
* | Put the "fix" tactic in the monad. | 2016-05-16 | |
| | |||
* | Put the "clear" tactic into the monad. | 2016-05-16 | |
| | |||
* | Actually using the symbol information to print Tactic Notations properly. | 2016-05-08 | |
| | |||
* | Removing dead code in Pptactic. | 2016-05-08 | |
| | |||
* | Pass user symbol to tactic notation printers. | 2016-05-08 | |
| | |||
* | Removing dead code and unused opens. | 2016-05-08 | |
| | |||
* | Normalizing the names of dynamic types to follow a typ_* scheme. | 2016-05-04 | |
| | |||
* | Removing useless generic arguments. | 2016-05-04 | |
| | |||
* | Moving the Val module to Geninterp. | 2016-05-04 | |
| | |||
* | Switching to an untyped toplevel representation for Ltac values. | 2016-05-04 | |
| | |||
* | Merge branch 'v8.5' | 2016-05-04 | |
|\ | |||
| * | Remove extraneous space in coqtop/pg output (bug #4675). | 2016-05-03 | |
| | | |||
* | | Revert "A heuristic to add parentheses in the presence of rules such as" | 2016-04-27 | |
| | | | | | | | | This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15. | ||
* | | Revert "So as to beautify to work, do not use notations in Inductive types" | 2016-04-27 | |
| | | | | | | | | This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98. | ||
* | | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | 2016-04-27 | |
| | | | | | | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244. | ||
* | | Revert "Temporary deactivate re-interpretation of terms in beautify." | 2016-04-27 | |
| | | | | | | | | This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81. | ||
* | | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and" | 2016-04-27 | |
| | | | | | | | | This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27. | ||
* | | Revert "Fixing printing of pat%constr." | 2016-04-27 | |
| | | | | | | | | This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c. | ||
* | | Revert "Fixing printing of induction/destruct as." | 2016-04-27 | |
| | | | | | | | | This reverts commit 691dc7d88c6810333eecef7c2f0b8d8617d19ab1. | ||
* | | Revert "Fixing extra space in printing destruct/induction as." | 2016-04-27 | |
| | | | | | | | | This reverts commit 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907. | ||
* | | Revert "Fixing printing of inversion as." | 2016-04-27 | |
| | | | | | | | | This reverts commit 6da8866a4fd79029b22bd1bf7cde6725a9ea259c. | ||
* | | Revert "Fixing printing of keeping hyp on the fly." | 2016-04-27 | |
| | | | | | | | | This reverts commit d408e09e5366899f4313f433cc9507ea92458c49. | ||
* | | Revert "Protect printing of intro-patterns from collision when "[|" or "|]"" | 2016-04-27 | |
| | | | | | | | | This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c. | ||
* | | Revert "Protect printing of ltac's "context [...]" from possible collision" | 2016-04-27 | |
| | | | | | | | | This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd. | ||
* | | Revert "Revert "Protect printing of intro-patterns from collision when "[|" or" | 2016-04-27 | |
| | | | | | | | | This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62. | ||
* | | Revert "Printing notations as parsed." | 2016-04-27 | |
| | | | | | | | | This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e. | ||
* | | Revert "Fixing printing of Arguments." | 2016-04-27 | |
| | | | | | | | | This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2. | ||
* | | Revert "Fixing printing of Polymorphic/Monomorphic." | 2016-04-27 | |
| | | | | | | | | This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933. | ||
* | | Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)." | 2016-04-27 | |
| | | | | | | | | This reverts commit d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4. | ||
* | | Revert "Fixing printing of Instance." | 2016-04-27 | |
| | | | | | | | | This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217. | ||
* | | Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword." | 2016-04-27 | |
| | | | | | | | | This reverts commit e11620ce155529c0e577304427f9b05d38e73caf. | ||
* | | Revert "Fixing extra space in printing bullets." | 2016-04-27 | |
| | | | | | | | | This reverts commit 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc. | ||
* | | Revert "Removing unused generalization of pr_vernac over pr_constr and ↵ | 2016-04-27 | |
| | | | | | | | | | | | | pr_lconstr." This reverts commit ee882d4cf6e7d84dc4589535042bbefdec56a288. | ||
* | | Revert "Simplification in ppvernac.ml." | 2016-04-27 | |
| | | | | | | | | This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74. | ||
* | | Revert "Isolating and exporting a function for printing body of a recursive ↵ | 2016-04-27 | |
| | | | | | | | | | | | | definition." This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673. | ||
* | | Revert "Fixing printing of Register retroknowledge." | 2016-04-27 | |
| | | | | | | | | This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb. | ||
* | | Revert "Passing around the precedence to the generic printer so as to solve" | 2016-04-27 | |
| | | | | | | | | This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1. | ||
* | | Revert "Temporary hack to restore missing printing of "constr:" in right-hand" | 2016-04-27 | |
| | | | | | | | | This reverts commit 90252e973f5bcafc5f3b0b18564612d7fb4503a8. | ||
* | | Revert "Taking into account the original grammar rule to print generic" | 2016-04-27 | |
| | | | | | | | | This reverts commit 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90. | ||
* | | Revert "Fixing extra space in front of terminal in printing vernac." | 2016-04-27 | |
| | | | | | | | | This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c. | ||
* | | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵ | 2016-04-27 | |
| | | | | | | | | | | | | EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64. | ||
* | | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and" | 2016-04-27 | |
| | | | | | | | | This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462. | ||
* | | Fixing extra space in front of terminal in printing vernac. | 2016-04-27 | |
| | | | | | | | | fix au revert [||] | ||
* | | Taking into account the original grammar rule to print generic | 2016-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-hand | 2016-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 solve | 2016-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. | 2016-04-27 | |
| | | |||
* | | Isolating and exporting a function for printing body of a recursive definition. | 2016-04-27 | |
| | | |||
* | | Simplification in ppvernac.ml. | 2016-04-27 | |
| | |