aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Collapse)Author
2016-06-16Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-06-16Fixing printing of inversion as.Hugo Herbelin
2016-06-16Fixing extra space in printing destruct/induction as.Hugo Herbelin
2016-06-16Fixing printing of induction/destruct as.Hugo Herbelin
2016-06-16Fixing printing of pat%constr.Hugo Herbelin
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Merge remote-tracking branch 'github/pr/194' into trunkMaxime Dénès
2016-06-15Remove the syntax changes introduced by this branch.Pierre-Marie Pédrot
We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6.
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
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-07Adding an only printing flag to notations.Pierre-Marie Pédrot
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 03:52:24 +0000