| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-03 | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug. | Matej Kosik | |
| 2016-05-02 | Generate 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-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-02 | Useless code in Tacentries. | Pierre-Marie Pédrot | |
| 2016-04-29 | Reduce 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-29 | Fix 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-28 | Make 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-28 | Update tutorial (fix bug #4699). | Guillaume Melquiond | |
| 2016-04-28 | Fix missing newline in coqchk engagement (bug #4694). | Guillaume Melquiond | |
| 2016-04-28 | An example for cd139311e, showing a consequence of not converting | Hugo Herbelin | |
| constants up to their canonical name (taken from Daniel's formalization of Puiseux theorem). | |||
| 2016-04-27 | Revert "A heuristic to add parentheses in the presence of rules such as" | Hugo Herbelin | |
| This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15. | |||
| 2016-04-27 | Revert "Not taking arguments given by name or position into account when" | Hugo Herbelin | |
| This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152. | |||
| 2016-04-27 | Revert "Adding a target for beautification." | Hugo Herbelin | |
| This reverts commit c2249c3b4c3387a3c8510e68fc447274d7299695. | |||
| 2016-04-27 | Revert "Adding a target check-beautify for testing reparsability of" | Hugo Herbelin | |
| This reverts commit 973b6c69f0861c113f7bd5b94604d2497520a334. | |||
| 2016-04-27 | Revert "So as to beautify to work, do not use notations in Inductive types" | Hugo Herbelin | |
| This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98. | |||
| 2016-04-27 | Revert "Protect the beautifier from change in the lexer state (typically by" | Hugo Herbelin | |
| This reverts commit f2192b492ca5407e740cf9d9d8696da89c978b93. | |||
| 2016-04-27 | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it" | Hugo Herbelin | |
| This reverts commit c4d1e3113f77af2e5474fe5676c272050dd445e5. | |||
| 2016-04-27 | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin | |
| This reverts commit bde36d4b00185065628324d8ca71994f84eae244. | |||
| 2016-04-27 | Revert "Being defensive in printing implicit arguments also with manual" | Hugo Herbelin | |
| This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565. | |||
| 2016-04-27 | Revert "Temporary deactivate re-interpretation of terms in beautify." | Hugo Herbelin | |
| This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81. | |||
| 2016-04-27 | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and" | Hugo Herbelin | |
| This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27. | |||
| 2016-04-27 | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an" | Hugo Herbelin | |
| This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff. | |||
| 2016-04-27 | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ↵ | Hugo Herbelin | |
| the levels." This reverts commit b6db76517b9a7f21078ab59a0b8eeee6bfdf5ba7. | |||
| 2016-04-27 | Revert "Fixing printers for pr_auto_using and pr_firstorder_using." | Hugo Herbelin | |
| This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda. | |||
| 2016-04-27 | Revert "Fixing printing of pat%constr." | Hugo Herbelin | |
| This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c. | |||
| 2016-04-27 | Revert "Fixing printing of induction/destruct as." | Hugo Herbelin | |
| This reverts commit 691dc7d88c6810333eecef7c2f0b8d8617d19ab1. | |||
| 2016-04-27 | Revert "Fixing extra space in printing destruct/induction as." | Hugo Herbelin | |
| This reverts commit 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907. | |||
| 2016-04-27 | Revert "Fixing printing of inversion as." | Hugo Herbelin | |
| This reverts commit 6da8866a4fd79029b22bd1bf7cde6725a9ea259c. | |||
| 2016-04-27 | Revert "Fixing printing of keeping hyp on the fly." | Hugo Herbelin | |
| This reverts commit d408e09e5366899f4313f433cc9507ea92458c49. | |||
| 2016-04-27 | Revert "Fixing parsing of constr argument of ltac functions at level 8 in the" | Hugo Herbelin | |
| This reverts commit e01dabf9f7aa530c4c70aadf464097cd102b1df6. | |||
| 2016-04-27 | Revert "Protect printing of intro-patterns from collision when "[|" or "|]"" | Hugo Herbelin | |
| This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c. | |||
| 2016-04-27 | Revert "Protect printing of ltac's "context [...]" from possible collision" | Hugo Herbelin | |
| This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd. | |||
| 2016-04-27 | Revert "Revert "Protect printing of intro-patterns from collision when "[|" or" | Hugo Herbelin | |
| This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62. | |||
| 2016-04-27 | Revert "Printing notations as parsed." | Hugo Herbelin | |
| This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e. | |||
| 2016-04-27 | Revert "Fixing printing of Arguments." | Hugo Herbelin | |
| This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2. | |||
| 2016-04-27 | Revert "Fixing printing of Polymorphic/Monomorphic." | Hugo Herbelin | |
| This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933. | |||
| 2016-04-27 | Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)." | Hugo Herbelin | |
| This reverts commit d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4. | |||
| 2016-04-27 | Revert "Fixing printing of Instance." | Hugo Herbelin | |
| This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217. | |||
| 2016-04-27 | Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword." | Hugo Herbelin | |
| This reverts commit e11620ce155529c0e577304427f9b05d38e73caf. | |||
| 2016-04-27 | Revert "Fixing extra space in printing bullets." | Hugo Herbelin | |
| This reverts commit 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc. | |||
| 2016-04-27 | Revert "Removing unused generalization of pr_vernac over pr_constr and ↵ | Hugo Herbelin | |
| pr_lconstr." This reverts commit ee882d4cf6e7d84dc4589535042bbefdec56a288. | |||
| 2016-04-27 | Revert "Simplification in ppvernac.ml." | Hugo Herbelin | |
| This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74. | |||
| 2016-04-27 | Revert "Isolating and exporting a function for printing body of a recursive ↵ | Hugo Herbelin | |
| definition." This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673. | |||
| 2016-04-27 | Revert "Fixing printing of Function." | Hugo Herbelin | |
| This reverts commit cb6f036b8e097085a849f806aa7c2627b789bd1f. | |||
| 2016-04-27 | Revert "Adding printers for ring and field commands." | Hugo Herbelin | |
| This reverts commit 9df1a3cf26d78df507d0e35c2d9ca987151777be. | |||
| 2016-04-27 | Revert "Fixing Add Parametric Relation by adding printer for binders." | Hugo Herbelin | |
| This reverts commit 36fb3d3a53418a81675815e47b3810e11bc31e4c. | |||
| 2016-04-27 | Revert "Fixing printing of Register retroknowledge." | Hugo Herbelin | |
| This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb. | |||
| 2016-04-27 | Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a" | Hugo Herbelin | |
| This reverts commit df1e24f64f68318221d08246098837368ee1b406. | |||
| 2016-04-27 | Revert "Passing around the precedence to the generic printer so as to solve" | Hugo Herbelin | |
| This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1. | |||
| 2016-04-27 | Revert "Temporary hack to compensate missing comma while re-printing tactic" | Hugo Herbelin | |
| This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |