aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Collapse)Author
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-07printing.mllib: remove some other .mli-only from a .mllibPierre Letouzey
2016-06-06Fixing problems introduced in 8.5 with Ltac trace report. E.g.Hugo Herbelin
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. g I. (* Was printing Top.Top#<>#1 *) idtac; f I. (* Was not properly locating error *) This is a "a minima" fix. This a different fix than in trunk, so the merge will have to take the trunk version.
2016-06-06About printing of traces of failures while calling ltac code.Hugo Herbelin
An Ltac trace printing mechanism was introduced in 8.4 which was inadvertedly modified by a series of commits such as 8e10368c3, 91f44f1da7a, ... It was also sometimes buggy, iirc, when entering ML tactics which themselves were calling ltac code. It got really bad in 8.5 as in: Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. idtac; f I. (* bad location reporting *) g I. (* was referring to tactic name "Top.Top#<>#1" *) which this commit fixes. I don't have a clear idea of what would be the best ltac tracing mechanism, but to avoid it to be broken without being noticed, I started to add some tests. Eventually, it might be worth that an Ltac expert brainstrom on it!
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
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.
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-06-02Move ide serialization libraries from lib/ to ide/Emilio Jesus Gallego Arias
This makes the core free from particular protocol choices. It should help with the ppx serialization project and shrinks clib.cma a bit.
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
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.
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
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.
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-08Actually using the symbol information to print Tactic Notations properly.Pierre-Marie Pédrot
2016-05-08Removing dead code in Pptactic.Pierre-Marie Pédrot
2016-05-08Pass user symbol to tactic notation printers.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
2016-04-27Revert "So as to beautify to work, do not use notations in Inductive types"Hugo Herbelin
This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98.
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
2016-04-27Revert "Temporary deactivate re-interpretation of terms in beautify."Hugo Herbelin
This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81.
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
2016-04-27Revert "Fixing printing of pat%constr."Hugo Herbelin
This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
2016-04-27Revert "Fixing printing of induction/destruct as."Hugo Herbelin
This reverts commit 691dc7d88c6810333eecef7c2f0b8d8617d19ab1.
2016-04-27Revert "Fixing extra space in printing destruct/induction as."Hugo Herbelin
This reverts commit 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907.
2016-04-27Revert "Fixing printing of inversion as."Hugo Herbelin
This reverts commit 6da8866a4fd79029b22bd1bf7cde6725a9ea259c.
2016-04-27Revert "Fixing printing of keeping hyp on the fly."Hugo Herbelin
This reverts commit d408e09e5366899f4313f433cc9507ea92458c49.
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Hugo Herbelin
This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c.
2016-04-27Revert "Protect printing of ltac's "context [...]" from possible collision"Hugo Herbelin
This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd.
2016-04-27Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Hugo Herbelin
This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62.
2016-04-27Revert "Printing notations as parsed."Hugo Herbelin
This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e.
2016-04-27Revert "Fixing printing of Arguments."Hugo Herbelin
This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2.
2016-04-27Revert "Fixing printing of Polymorphic/Monomorphic."Hugo Herbelin
This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933.
2016-04-27Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Hugo Herbelin
This reverts commit d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4.
2016-04-27Revert "Fixing printing of Instance."Hugo Herbelin
This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217.
2016-04-27Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Hugo Herbelin
This reverts commit e11620ce155529c0e577304427f9b05d38e73caf.
2016-04-27Revert "Fixing extra space in printing bullets."Hugo Herbelin
This reverts commit 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc.
2016-04-27Revert "Removing unused generalization of pr_vernac over pr_constr and ↵Hugo Herbelin
pr_lconstr." This reverts commit ee882d4cf6e7d84dc4589535042bbefdec56a288.
2016-04-27Revert "Simplification in ppvernac.ml."Hugo Herbelin
This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74.
2016-04-27Revert "Isolating and exporting a function for printing body of a recursive ↵Hugo Herbelin
definition." This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673.
2016-04-27Revert "Fixing printing of Register retroknowledge."Hugo Herbelin
This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb.
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 08:30:15 +0000