aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
...
* | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | | | | | | | | | | | | | | | Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
* | | 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
| | | | | | | | | | | | | | | | | | | | | This makes the core free from particular protocol choices. It should help with the ppx serialization project and shrinks clib.cma a bit.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\| |
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| * | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
| | | | | | | | | | | | | | | | | | | | | Return the most appropriate evar_map for commands that can run on non-focused proofs (like Check, Show and debug printers) so that universes and existentials are printed correctly (they are global to the proof). The API is backwards compatible.
* | | 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
| | | | | | | | | | | | 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 [||]
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:43:54 +0000