aboutsummaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
AgeCommit message (Collapse)Author
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
2016-04-27Fixing printing of induction/destruct as.Hugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
VERNAC EXTEND.
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
variables" when matching over "{v : _ | _ & _}" which hides twice the binding "fun v" since it is "sig2 (fun v => _) (fun v => _)". Computing the bound variables statically at internalisation time rather than every time at interpretation time. This cannot hurt even if I don't know how to deal with the "notation" problem of a single bound variable actually hiding two: at the current time, the notation is printed only if the two variables are identical (see #4592), so, with this semantics the warning should not be printed, but we lost the information that we are coming from a notation; if #4592 were addressed, then one of the binding should be alpha-renamed if they differ, so collision should be solved by choosing the variable name which is not renamed, but the matching algorithm should then be aware of what the notation printing algorithm is doing... maybe not the most critical thing at the current time.
2016-04-25Removing dead code related to printing of ML tactics in Pptactic.Pierre-Marie Pédrot
2016-04-12Fixing printing of "destruct in" after ce71ac17268f.Hugo Herbelin
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning.
2016-04-10Extruding the print_atom primitive.Pierre-Marie Pédrot
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Removing automatic printing of leading space in auto_using andHugo Herbelin
hintbases so that it does not put extra space when auto is defined as a TACTIC EXTEND.
2016-04-09In pr_clauses, do not print a leading space by default so that it canHugo Herbelin
be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND.
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all.
2016-04-08Fixing printing of Tactic Notations with tactic arguments.Pierre-Marie Pédrot
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-19Removing the untyped representation of genargs.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-04Removing the UConstr entry of the tactic_arg AST.Pierre-Marie Pédrot
This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there.
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-08 01:57:17 +0000