aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-04-27Revert "Protect printing of ltac's "context [...]" from possible collision"Hugo Herbelin
This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd.
2016-04-27Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Hugo Herbelin
This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62.
2016-04-27Revert "Printing notations as parsed."Hugo Herbelin
This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e.
2016-04-27Revert "Fixing printing of Arguments."Hugo Herbelin
This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2.
2016-04-27Revert "Fixing printing of Polymorphic/Monomorphic."Hugo Herbelin
This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933.
2016-04-27Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Hugo Herbelin
This reverts commit d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4.
2016-04-27Revert "Fixing printing of Instance."Hugo Herbelin
This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217.
2016-04-27Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Hugo Herbelin
This reverts commit e11620ce155529c0e577304427f9b05d38e73caf.
2016-04-27Revert "Fixing extra space in printing bullets."Hugo Herbelin
This reverts commit 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc.
2016-04-27Revert "Removing unused generalization of pr_vernac over pr_constr and ↵Hugo Herbelin
pr_lconstr." This reverts commit ee882d4cf6e7d84dc4589535042bbefdec56a288.
2016-04-27Revert "Simplification in ppvernac.ml."Hugo Herbelin
This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74.
2016-04-27Revert "Isolating and exporting a function for printing body of a recursive ↵Hugo Herbelin
definition." This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673.
2016-04-27Revert "Fixing printing of Function."Hugo Herbelin
This reverts commit cb6f036b8e097085a849f806aa7c2627b789bd1f.
2016-04-27Revert "Adding printers for ring and field commands."Hugo Herbelin
This reverts commit 9df1a3cf26d78df507d0e35c2d9ca987151777be.
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".
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 03:17:57 +0000