aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
...
* | | 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 [||]
* | | Taking into account the original grammar rule to print genericGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | arguments of vernac extensions, so that in list with a separator, the separator is printed.
* | | Temporary hack to restore missing printing of "constr:" in right-handGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Passing around the precedence to the generic printer so as to solveGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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".
* | | Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | No other changes (long only because of a change of indentation).
* | | Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | Fixing : in Declare Module.
* | | Fixing printing of Instance.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing printing of Arguments.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Printing notations as parsed.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Revert "Protect printing of intro-patterns from collision when "[|" orGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "|]"" because this commit triggers a Error: Files proofs/proofs.cma(Miscprint) and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer) make inconsistent assumptions over interface Lexer Adding two extra spaces systematically instead. This reverts commit 72be1f6beafafc3edd30df673fbb6c7e88f8fac7.
* | | Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | with user-level notations by inserting spaces.
* | | Protect printing of intro-patterns from collision when "[|" or "|]"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | exist as a keyword by inserting a space inbetween.
* | | Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing printing of inversion as.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | VERNAC EXTEND.
* | | Temporary deactivate re-interpretation of terms in beautify.Gravatar Hugo Herbelin2016-04-27
| | |
* | | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* | | So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance.
* | | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Notation "## c" := (S c) (at level 0, c at level 100). which break the stratification of precedences. This works for the case of infix or suffix operators which occur in only one grammar rule, such as +, *, etc. This solves the "constr" part of #3709, even though this example is artificial. The fix is not complete. It puts extra parenthesese even when it is end of sentence, as in Notation "# c % d" := (c+d) (at level 3). Check fun x => # ## x % ## (x * 2). (* fun x : nat => # ## x % (## x * 2) *) The fix could be improved by not always using 100 for the printing level of "## c", but 100 only when not the end of the sentence. The fix does not solve the general problem with symbols occurring in more than one rule, as e.g. in: Notation "# c % d" := (c+d) (at level 1). Notation "## c" := (S c) (at level 0, c at level 5). Check fun x => # ## x % 0. (* Parentheses are necessary only if "0 % 0" is also parsable *) I don't see in this case what better approach to follow than restarting the parser to check reversibility of the printing.
* | | Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 01:06:42 +0000