aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-04-27Revert "Fixing printing of inversion as."Hugo Herbelin
This reverts commit 6da8866a4fd79029b22bd1bf7cde6725a9ea259c.
2016-04-27Revert "Fixing printing of keeping hyp on the fly."Hugo Herbelin
This reverts commit d408e09e5366899f4313f433cc9507ea92458c49.
2016-04-27Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Hugo Herbelin
This reverts commit e01dabf9f7aa530c4c70aadf464097cd102b1df6.
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Hugo Herbelin
This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 09:27:57 +0000