| Commit message (Collapse) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | Do not export an internal function in Namegen. |  Pierre-Marie Pédrot | 2016-08-25 | |
| | | | ||||
| * | | Properly compute types for assumed section variables (bug #5035). |  Guillaume Melquiond | 2016-08-24 | |
| | | | | | | | | | | | | | | | | | | | | | This bug was introduced by commit 34ef02fac1110673ae74c41c185c228ff7876de2 Author: Matej Kosik <m4tej.kosik@gmail.com> Date: Fri Jan 29 10:13:12 2016 +0100 CLEANUP: Context.{Rel,Named}.Declaration.t | |||
| * | | Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6 | Pierre-Marie Pédrot | 2016-08-24 | |
| |\ \ | ||||
| * \ \ | Merge PR #258: "Fix newline issues" into v8.6 | Pierre-Marie Pédrot | 2016-08-24 | |
| |\ \ \ | ||||
| * | | | | Fix bug #4914: LtacProf printout has too many newlines. | Pierre-Marie Pédrot | 2016-08-23 | |
| | | | | | ||||
| * | | | | Arguments: give / after last ! error detection fixed |  Enrico Tassi | 2016-08-23 | |
| | | | | | ||||
| * | | | | fix get_host_port error message (#4724) | Enrico Tassi | 2016-08-23 | |
| | | | | | ||||
| * | | | | update Proof General URL |  Paul Steckler | 2016-08-23 | |
| | | | | | ||||
| * | | | | Fix bug #4904: [Import] does not load intermediately unqualified names of ↵ | Pierre-Marie Pédrot | 2016-08-23 | |
| | | | | | | | | | | | | | | | | | aliases. | |||
| * | | | | Fast path for set operations. | Pierre-Marie Pédrot | 2016-08-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | We consider an approximation of the size of sets before choosing the most appropriate algorithm. This drastically affects some universe-polymorphic code which was doing a lot of set operations on disimilar sizes. | |||
| * | | | | Merge remote-tracking branch 'github/pr/261' into v8.6 |  Maxime Dénès | 2016-08-22 | |
| |\ \ \ \ | | | | | | | | | | | | | | | | Was PR#261: Use a better data structure for VM compilation of free vars. | |||
| | * | | | | Use a better data structure for VM compilation of free vars. | Pierre-Marie Pédrot | 2016-08-22 | |
| |/ / / / | | | | | | | | | | | | | This fixes #3450 and probably provides a huge speed-up to many instances. | |||
| * | | | | Pushing error backtrace in unification reraise. | Pierre-Marie Pédrot | 2016-08-22 | |
| | | | | | ||||
| * | | | | Documenting "Set Structural Injection". |  Hugo Herbelin | 2016-08-21 | |
| | | | | | ||||
| * | | | | Do not recompute the whole evar naming environment in GProd intepretation. | Pierre-Marie Pédrot | 2016-08-21 | |
| | | | | | ||||
| * | | | | Short path for Pretyping.ltac_interp_name_env. | Pierre-Marie Pédrot | 2016-08-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of recomputing the evar name environment from scratch when it is unchanged, we simply return the original one. This should fix #4964 for good, although I still find the global evar naming mechanism from Pretyping more than messy. Introducing the heuristic allowing to capture variables from Ltac in constr binders is indeed the root of many evils... That is far from being a zero-cost abstraction! | |||
| * | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-08-21 | |
| |\ \ \ \ | | |_|/ | |/| | | ||||
| * | | | | More standard naming for the Imparg.with_implicits function. | Pierre-Marie Pédrot | 2016-08-20 | |
| | | | | | ||||
| * | | | | Fixing a bug in the presence of let-in while inferring the return clause. | Hugo Herbelin | 2016-08-20 | |
| | | | | | ||||
| | * | | | Fixing an anomaly in printing a unification error message. | Hugo Herbelin | 2016-08-20 | |
| | | | | | ||||
| * | | | | Test file for bug #4187. | Pierre-Marie Pédrot | 2016-08-19 | |
| | | | | | ||||
| * | | | | Fix performance bug: do not compute implicits of abstracted lemmas. | Pierre-Marie Pédrot | 2016-08-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | This was showing up in some of Jason's examples, where an abstract had to compute the weak head form of a huge term in order to find the corresponding implicit arguments. | |||
| * | | | | Removing dead code in Impargs. | Pierre-Marie Pédrot | 2016-08-19 | |
| | | | | | ||||
| | | | * | [pp] Fix bug 4842 (Time prints in multiple lines) |  Emilio Jesus Gallego Arias | 2016-08-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit proposes a fix for https://coq.inria.fr/bugs/show_bug.cgi?id=4842 The previous feature is a bit complicated to do correctly due to the separation over who has control of the console. Indeed, `-timed` is a command line option of the batch compiler, so we resort to a hack and assume control over the console. I am not very happy with this solution but should do the job. Note that the timing event is still being sent by the standard msg mechanism. A particular point of interest is the duplication of paths between the stm and vernac. | |||
| * | | | | Merge remote-tracking branch 'origin/pr/246' into v8.6 |  Matthieu Sozeau | 2016-08-19 | |
| |\ \ \ \ | ||||
| * | | | | | Moving Taccoerce to ltac/ folder. | Pierre-Marie Pédrot | 2016-08-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | This was an overlook. There was no reason to let it in the tactics/ folder, as is was semantically part of the Ltac implementation. | |||
| | | * | | | Remove extraneous dot in error message (bug #4832). | Guillaume Melquiond | 2016-08-19 | |
| | | | | | | ||||
| * | | | | | Fix anomaly on user-inputted projection name (bug #5029). | Guillaume Melquiond | 2016-08-19 | |
| | |_|_|/ |/| | | | ||||
| | | | * | [pp] Fix newline issues. | Emilio Jesus Gallego Arias | 2016-08-19 | |
| | |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where we got a few cases wrong wrt to newline endings. Thanks to @herbelin for pointing it out. This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842 | |||
| * | | | Merge remote-tracking branch 'github/bug4978' into v8.6 | Matthieu Sozeau | 2016-08-18 | |
| |\ \ \ | ||||
| * \ \ \ | Merge remote-tracking branch 'github/bug4188' into v8.6 | Matthieu Sozeau | 2016-08-18 | |
| |\ \ \ \ | ||||
| | | | | * | Fix incorrect glob data for module symbols (bug #2336). | Guillaume Melquiond | 2016-08-18 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The logic was backward: if the path of a symbol was a prefix of the current path, then the current path (without sections) was used. But what we want is that, if the current path (without sections) is a prefix of the path of a symbol, then the former should be used. This fixes about 1,600 broken links in the documentation of the standard library. | |||
| * | | | | | Fix an occurrence of deprecated eqn syntax in stdlib. | Maxime Dénès | 2016-08-18 | |
| | | | | | | ||||
| * | | | | | Fix bug #4939: LtacProf prints tactic notations weirdly. | Pierre-Marie Pédrot | 2016-08-18 | |
| | | | | | | ||||
| * | | | | | Adding a test for bug #4653. | Pierre-Marie Pédrot | 2016-08-18 | |
| | | | | | | ||||
| * | | | | | Merge PR #256 into v8.6 | Pierre-Marie Pédrot | 2016-08-18 | |
| |\ \ \ \ \ | ||||
| | * | | | | | In docs, fix command to reset Ltac profiling | Paul Steckler | 2016-08-17 | |
| |/ / / / / | ||||
| | * | | | | Fix setoid_rewrite to raise proper errors | Matthieu Sozeau | 2016-08-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | when the rewrite lemma doesn't typecheck or does not correspond to a relation. | |||
| | | | | * | Fixing #5001 (metas not cleaned properly in clenv_refine_in). | Hugo Herbelin | 2016-08-17 | |
| | | | | | | | | | | | | | | | | | | | | | Fixing by copying what Matthieu did for Clenvtac.clenv_refine. | |||
| | | | | * | Fixing CHANGES. | Hugo Herbelin | 2016-08-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section. | |||
| * | | | | | Documenting fix of #3070 (subst and chain of dependencies). | Hugo Herbelin | 2016-08-17 | |
| |/ / / / | ||||
| | * / / | Fix #4978: priorities of Equivalence instances | Matthieu Sozeau | 2016-08-17 | |
| |/ / / | ||||
| * | | | Fixing #3070 ("subst" taking properly into account chains of dependencies). | Hugo Herbelin | 2016-08-17 | |
| | | | | ||||
| * | | | Two protections against failures when printing evar_map. | Hugo Herbelin | 2016-08-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | Delimit the scope of the failure to ease potential need for debugging the debugging printer. Protect against one of the causes of failure (calling get_family_sort_of with non-synchronized sigma). | |||
| * | | | Fixing printing in debugger (no global env in debugger). | Hugo Herbelin | 2016-08-17 | |
| | | | | ||||
| * | | | A fix to dev/include. | Hugo Herbelin | 2016-08-17 | |
| | | | | ||||
| | | * | infoH: output via msg_* to make the XML protocol happy | Enrico Tassi | 2016-08-17 | |
| | | | | ||||
| * | | | Removing dead unsafe debugging code in Constrintern. | Pierre-Marie Pédrot | 2016-08-16 | |
| | | | | ||||
| | | * | Output a break before a list only if there was an empty line (bug #4606). | Guillaume Melquiond | 2016-08-16 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Moreover, this commit makes sure that an empty line after a list is always translated into a break. ("StartLevel 1" was excluded, for some reason.) It also avoids some code duplication. In particular, "stop_item ()" is defined as "reach_item_level 0", so there is no reason to handle "StartLevel 1" specially. | |||
| * | | | Merge PR #250 into v8.6 | Pierre-Marie Pédrot | 2016-08-16 | |
| |\ \ \ | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |