aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-04-27Revert "Revert "Re-add -beautify by default.""Hugo Herbelin
This reverts commit 67335c832a55cbd0ca559906bbe1af2485241353.
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 "More abstraction in cases.mli."Hugo Herbelin
This reverts commit 975e2a05050c704161aca3fbac96376eeda6fb4a.
2016-04-27Revert "Add support for generalization also on named variables in ↵Hugo Herbelin
pattern-matching" This reverts commit be80899499094fc8a15362931e3cec650f2fb14e.
2016-04-27Revert "Add support for deep dependencies in variables within the recursive ↵Hugo Herbelin
structure." This reverts commit eaca8dadf7dd8152a86f4fc75631754344268dbf.
2016-04-27Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Hugo Herbelin
This reverts commit 94e9e28ebaa33e11164ca07f225d998ca7f8e52c.
2016-04-27Revert "Using existing names as a basis for the inner names of the ↵Hugo Herbelin
pattern-matching produced by an implicit "in" clause" This reverts commit ba9f53314ff6132d0013e53879395e0dc9d8038c.
2016-04-27Revert "Vers un filtrage profond ..."Hugo Herbelin
This reverts commit d9f0daefb437955df8102de2b3c4c31749b6946e.
2016-04-27Vers un filtrage profond ...Hugo Herbelin
2016-04-27Using existing names as a basis for the inner names of the pattern-matching ↵Hugo Herbelin
produced by an implicit "in" clause
2016-04-27Fixing a De Bruijn bug in computing return predicate by inversion.Hugo Herbelin
2016-04-27Add support for deep dependencies in variables within the recursive structure.Hugo Herbelin
2016-04-27Add support for generalization also on named variables in pattern-matchingHugo Herbelin
algorithm.
2016-04-27More abstraction in cases.mli.Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
2016-04-27Revert "Re-add -beautify by default."Hugo Herbelin
This reverts commit 1171590c544492842a848c6765b61c70fca19a01.
2016-04-27Fixing a mispelling coma -> comma.Hugo Herbelin
2016-04-27Typo in comment.Hugo Herbelin
2016-04-27Fixing space in an error message.Hugo Herbelin
2016-04-27Warn about possible shadowing of a name occurring in a "in" clause.Hugo Herbelin
2016-04-27When interpreting "match goal with ... end" in ltac, expand evars byHugo Herbelin
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".
2016-04-27Re-add -beautify by default.Hugo Herbelin
2016-04-27Add plugins to Makefile.Hugo Herbelin
2016-04-27Fixing extra space in front of terminal in printing vernac.Hugo Herbelin
fix au revert [||]
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-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
"exists c1, c2".
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-27A fix to #3709: ensuring extra parentheses when a tactic entry has aHugo Herbelin
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.
2016-04-27Fixing printing of Register retroknowledge.Hugo Herbelin
2016-04-27Fixing Add Parametric Relation by adding printer for binders.Hugo Herbelin
2016-04-27Adding printers for ring and field commands.Hugo Herbelin
2016-04-27Fixing printing of Function.Hugo Herbelin
2016-04-27Isolating and exporting a function for printing body of a recursive definition.Hugo Herbelin
2016-04-27Simplification in ppvernac.ml.Hugo Herbelin
2016-04-27Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
No other changes (long only because of a change of indentation).
2016-04-27Fixing extra space in printing bullets.Hugo Herbelin
2016-04-27Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
Fixing : in Declare Module.
2016-04-27Fixing printing of Instance.Hugo Herbelin
2016-04-27Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-04-27Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-04-27Fixing printing of Arguments.Hugo Herbelin
2016-04-27Printing notations as parsed.Hugo Herbelin
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" orHugo Herbelin
"|]"" 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.
2016-04-27Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
with user-level notations by inserting spaces.
2016-04-27Protect printing of intro-patterns from collision when "[|" or "|]"Hugo Herbelin
exist as a keyword by inserting a space inbetween.
2016-04-27Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
presence of entries starting with a non-terminal such as "b ^2".
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-03-08 04:49:31 +0000