aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-05-03setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug.Matej Kosik
2016-05-03Call hooks when terminating a definition proof (bug #4663).Guillaume Melquiond
Also register properly the kind of definition.
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-05-02Make votour a bit more robust/forgiving with respect to user commands (bug ↵Guillaume Melquiond
#4702).
2016-05-02Properly handle notations containing spaces (bug #4538).Guillaume Melquiond
When a notation was starting or ending a space, Coq assumed the notation had no terminal symbol in either places. Coq also considered a notation containing only spaces to be productive. As stated in the documentation, extraneous spaces are only meant as printing hints, they are not meant to have any influence on parsing.
2016-05-02Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Guillaume Melquiond
When encountering a "simpl nomatch" constant, the reduction machinery tries to unfold it. If the subsequent partial reduction does not produce any match construct, it keeps going from the reduced term. Unfortunately, the reduced term has been refolded in the meantime, which means that some of the previous reduction steps have been canceled, thus causing an infinite loop. This patch delays the refolding till the very end, so that reduction always progresses. Disclaimer: I have no idea what I am doing here. The patch compiles the standard library and the test suite properly, so hopefully they contain enough tests to exercise the reduction machinery.
2016-05-02Generate parsing rules for ML tactics in the same order as before a7917a32.Pierre-Marie Pédrot
Once again showing the fragility of the parsing engine, commit a7917a32 reversed the relative order of the declaration of parsing rules for tactics declared through TACTIC EXTEND. There is probably no good order at all, but for retrocompatibility, this patch enforces the original one.
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-02Useless code in Tacentries.Pierre-Marie Pédrot
2016-04-29Reduce ide/coq.png to 256x256.Guillaume Melquiond
Commit 1774a87 increased the file to 1024x1024. This had two adverse consequences. First, the icon was too large to be used as a window icon ("gdk_window_set_icon_list: icons too large"), so Coqide 8.5 no longer had an icon at runtime. Second, the file was also used in the About message box, which was thus exceeding the display size of any reasonably-priced device. This commit reverts the file to a saner size (still larger than the original 66x100 picture).
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
As noticed by Cyprien Mangin, projected terms cannot directly be used as head values. Indeed, they might be applications (e.g. constructors as in the bug report) whose arguments would thus be missing from the evaluation stack when doing any iota-reduction step. The only case where it would make sense is when the evaluation stack is empty, as an optimization. Indeed, in that case, the arguments are put on the stack, and then immediately put back inside the term.
2016-04-28Make the language grammar much more precise. (Fix bugs #4682 and #4683)Guillaume Melquiond
Rather than being isolated words, commands and tactics now extend till dot separators. So bullets can be defined as living only at the top level of proofs, which should make their detection much more robust.
2016-04-28Update tutorial (fix bug #4699).Guillaume Melquiond
2016-04-28Fix missing newline in coqchk engagement (bug #4694).Guillaume Melquiond
2016-04-28An example for cd139311e, showing a consequence of not convertingHugo Herbelin
constants up to their canonical name (taken from Daniel's formalization of Puiseux theorem).
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
2016-04-27Revert "Not taking arguments given by name or position into account when"Hugo Herbelin
This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152.
2016-04-27Revert "Adding a target for beautification."Hugo Herbelin
This reverts commit c2249c3b4c3387a3c8510e68fc447274d7299695.
2016-04-27Revert "Adding a target check-beautify for testing reparsability of"Hugo Herbelin
This reverts commit 973b6c69f0861c113f7bd5b94604d2497520a334.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 20:32:29 +0000