aboutsummaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
AgeCommit message (Collapse)Author
2016-12-02Fixing printing of "ltac:" in tactics after surrounding parenthesesHugo Herbelin
became mandatory.
2016-12-02Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
with user-level notations by inserting spaces.
2016-12-02More on fixing #5098 (preserving printing of "in hyp").Hugo Herbelin
2016-11-22Properly parenthesize "ltac:" arguments (bug #5169).Guillaume Melquiond
2016-10-08Fix bug #5098: Symmetry broken in HoTT.Pierre-Marie Pédrot
We defactorize the in_clause grammar entry to allow parsing of the "symmetry" tactic when it has no arguments. Beforehand, the clause_dft_concl entry accepted the empty stream, preventing the definition of symmetry as a mere identifier.
2016-09-16Addressing OCaml compilation warnings.Hugo Herbelin
One of them revealed a true bug.
2016-09-09Fix bug #4940: Tactic notation printing could be more informative.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Pierre Letouzey
module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
In pat%constr, creating new evars is now allowed only if "eintros" is given, i.e. "intros" checks that no evars are created, and similarly e.g. for "injection ... as ... pat%constr". The form "eintros [...]" or "eintros ->" with the case analysis or rewrite creating evars is now also supported. This is not a commitment to say that it is good to have an e- modifier to tactics. It is just to be consistent with the existing convention. It seems to me that the "no e-" variants are good for beginners. However, expert might prefer to use the e-variants by default. Opinions from teachers and users would be useful. To be possibly done: do that [= ...] work on hypotheses with side conditions or parameters based on the idea that they apply the full injection and not only the restriction of it to goals which are exactly an equality, as it is today.
2016-06-16Fixing missing substitution / printing cases of TacSelect.Pierre-Marie Pédrot
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-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-09Merge branch 'v8.5'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-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-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-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
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 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 ltac's "context [...]" from possible collision"Hugo Herbelin
This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd.
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.
2016-04-27Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Hugo Herbelin
This reverts commit 90252e973f5bcafc5f3b0b18564612d7fb4503a8.
2016-04-27Revert "Taking into account the original grammar rule to print generic"Hugo Herbelin
This reverts commit 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90.
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵Hugo Herbelin
EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
2016-04-27Taking into account the original grammar rule to print genericHugo Herbelin
arguments of vernac extensions, so that in list with a separator, the separator is printed.
2016-04-27Temporary hack to restore missing printing of "constr:" in right-handHugo Herbelin
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.
2016-04-27Passing around the precedence to the generic printer so as to solveHugo Herbelin
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".
2016-04-27Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
with user-level notations by inserting spaces.
2016-04-27Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-04-27Fixing printing of inversion as.Hugo Herbelin
2016-04-27Fixing extra space in printing destruct/induction as.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 21:43:27 +0000