aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-04-27Revert "So as to beautify to work, do not use notations in Inductive types"Hugo Herbelin
This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98.
2016-04-27Revert "Protect the beautifier from change in the lexer state (typically by"Hugo Herbelin
This reverts commit f2192b492ca5407e740cf9d9d8696da89c978b93.
2016-04-27Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"Hugo Herbelin
This reverts commit c4d1e3113f77af2e5474fe5676c272050dd445e5.
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
2016-04-27Revert "Being defensive in printing implicit arguments also with manual"Hugo Herbelin
This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565.
2016-04-27Revert "Temporary deactivate re-interpretation of terms in beautify."Hugo Herbelin
This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81.
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
2016-04-27Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Hugo Herbelin
This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff.
2016-04-27Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ↵Hugo Herbelin
the levels." This reverts commit b6db76517b9a7f21078ab59a0b8eeee6bfdf5ba7.
2016-04-27Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Hugo Herbelin
This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
2016-04-27Revert "Fixing printing of pat%constr."Hugo Herbelin
This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
2016-04-27Revert "Fixing printing of induction/destruct as."Hugo Herbelin
This reverts commit 691dc7d88c6810333eecef7c2f0b8d8617d19ab1.
2016-04-27Revert "Fixing extra space in printing destruct/induction as."Hugo Herbelin
This reverts commit 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 03:38:36 +0000