aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* More abstraction in cases.mli.Gravatar Hugo Herbelin2016-04-27
|
* Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
* Revert "Re-add -beautify by default."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 1171590c544492842a848c6765b61c70fca19a01.
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
|
* Typo in comment.Gravatar Hugo Herbelin2016-04-27
|
* Fixing space in an error message.Gravatar Hugo Herbelin2016-04-27
|
* Warn about possible shadowing of a name occurring in a "in" clause.Gravatar Hugo Herbelin2016-04-27
|
* When interpreting "match goal with ... end" in ltac, expand evars byGravatar Hugo Herbelin2016-04-27
| | | | | | | need at matching time rather than eagerly at the beginning of the call to "match". To be done for other constructs too, e.g. "match term with ... endp".
* Re-add -beautify by default.Gravatar Hugo Herbelin2016-04-27
|
* Add plugins to Makefile.Gravatar Hugo Herbelin2016-04-27
|
* 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.
* Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
| | | | "exists c1, c2".
* 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".
* A fix to #3709: ensuring extra parentheses when a tactic entry has aGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | subentry at a higher tactic level than the entry itself. This is applicable to the parsing of expressions with infix or postfix operators such as ; or ||. Could be improved, e.g. so that no parenthesis are put when the expression is the rightmost one, as in: now (tac1;tac2) where parentheses are not needed but still printed with this patch, while the patch adds needed parentheses in (now tac1);tac2 This would hardly scale to more complex grammars. E.g., if a suffix expression can extend a leading expression as part of different grammar entries, as in let x := simpl in y ... I don't see in general how to anticipate the need for parentheses without restarting the parser to check the reversibility of the printing.
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-04-27
|
* Fixing Add Parametric Relation by adding printer for binders.Gravatar Hugo Herbelin2016-04-27
|
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-04-27
|
* Fixing printing of Function.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 parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-04-27
| | | | presence of entries starting with a non-terminal such as "b ^2".
* 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
|
* Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-04-27
|
* In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Gravatar Hugo Herbelin2016-04-27
|
* Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-04-27
| | | | implicit is found whether one writes (sig P) or {x|P x}.
* 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
|
* Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-04-27
| | | | implicit arguments when in beautification mode.
* 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.
* Changing rule for "*" in Operator_Properties so that, iterated, itGravatar Hugo Herbelin2016-04-27
| | | | does not print to ** which is a keyword.
* Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-04-27
| | | | | calling Pcoq.parse_string, what some plugins such as coretactics, are doing, thus breaking the beautification of "Declare ML Module").
* 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.
* Adding a target check-beautify for testing reparsability ofGravatar Hugo Herbelin2016-04-27
| | | | | | beautification of the standard library. Currently not intrusive but needs two extra phases of compilation.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 10:19:29 +0000