aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-04-27Revert "Fixing Add Parametric Relation by adding printer for binders."Hugo Herbelin
This reverts commit 36fb3d3a53418a81675815e47b3810e11bc31e4c.
2016-04-27Revert "Fixing printing of Register retroknowledge."Hugo Herbelin
This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb.
2016-04-27Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Hugo Herbelin
This reverts commit df1e24f64f68318221d08246098837368ee1b406.
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 compensate missing comma while re-printing tactic"Hugo Herbelin
This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a.
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 "Fixing extra space in front of terminal in printing vernac."Hugo Herbelin
This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
2016-04-27Revert "Add plugins to Makefile."Hugo Herbelin
This reverts commit 5e9b37a815795efaafd64ab8fe19bf8560d70203.
2016-04-27Revert "Re-add -beautify by default."Hugo Herbelin
This reverts commit d28c1d7d908fe9d5fc719d58433a6b87c12390ba.
2016-04-27Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Hugo Herbelin
This reverts commit 7e613daf7c71a4180725bddb40151c2b5a6348f4.
2016-04-27Revert "Warn about possible shadowing of a name occurring in a "in" clause."Hugo Herbelin
This reverts commit 46f876a9404844487476415af2e6f6d938558d15.
2016-04-27Revert "Fixing space in an error message."Hugo Herbelin
This reverts commit e0fd6e50800bc5aec4eafddd315941d6f7bc6efc.
2016-04-27Revert "Typo in comment."Hugo Herbelin
This reverts commit 239f30c2070018db88e568acca6c9054f650ca38.
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 19:14:56 +0000