aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
|
* CLEANUP: removing superfluous (module) qualifiersGravatar Matej Kosik2016-08-24
|
* CLEANUP: removing unnecessary variable bindingGravatar Matej Kosik2016-08-24
|
* Changing the definition of the "Lib.variable.info" type to enable us to do ↵Gravatar Matej Kosik2016-08-24
| | | | more cleanups
* Merging a branch that adds "Context.Named.Declaration.to_rel" function.Gravatar Matej Kosik2016-08-24
|\
| * Adding "Context.Named.Declaration.to_rel" functionGravatar Matej Kosik2016-08-24
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-21
|\ \
| * \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
| |\ \
| * | | More standard naming for the Imparg.with_implicits function.Gravatar Pierre-Marie Pédrot2016-08-20
| | | |
| * | | Fixing a bug in the presence of let-in while inferring the return clause.Gravatar Hugo Herbelin2016-08-20
| | | |
| | * | Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
| | | |
| * | | Test file for bug #4187.Gravatar Pierre-Marie Pédrot2016-08-19
| | | |
| * | | Fix performance bug: do not compute implicits of abstracted lemmas.Gravatar Pierre-Marie Pédrot2016-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.Gravatar Pierre-Marie Pédrot2016-08-19
| | | |
| * | | Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
| |\ \ \
| * | | | Moving Taccoerce to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-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).Gravatar Guillaume Melquiond2016-08-19
| | | | |
| * | | | Fix anomaly on user-inputted projection name (bug #5029).Gravatar Guillaume Melquiond2016-08-19
| | | | |
| * | | | Merge remote-tracking branch 'github/bug4978' into v8.6Gravatar Matthieu Sozeau2016-08-18
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'github/bug4188' into v8.6Gravatar Matthieu Sozeau2016-08-18
| |\ \ \ \ \
| | | | | * | Fix incorrect glob data for module symbols (bug #2336).Gravatar Guillaume Melquiond2016-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.Gravatar Maxime Dénès2016-08-18
| | | | | | |
| * | | | | | Fix bug #4939: LtacProf prints tactic notations weirdly.Gravatar Pierre-Marie Pédrot2016-08-18
| | | | | | |
| * | | | | | Adding a test for bug #4653.Gravatar Pierre-Marie Pédrot2016-08-18
| | | | | | |
| * | | | | | Merge PR #256 into v8.6Gravatar Pierre-Marie Pédrot2016-08-18
| |\ \ \ \ \ \
| | * | | | | | In docs, fix command to reset Ltac profilingGravatar Paul Steckler2016-08-17
| |/ / / / / /
| | * | | | | Fix setoid_rewrite to raise proper errorsGravatar Matthieu Sozeau2016-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).Gravatar Hugo Herbelin2016-08-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixing by copying what Matthieu did for Clenvtac.clenv_refine.
| | | | | * | Fixing CHANGES.Gravatar Hugo Herbelin2016-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).Gravatar Hugo Herbelin2016-08-17
| |/ / / / /
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\| | | | |
* | | | | | Revert "CLEANUP: removing the definition of the ↵Gravatar Pierre-Marie Pédrot2016-08-17
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "Context.Rel.Declaration.to_tuple" function" This reverts commit 4b24bb7d3b770592015c264001b9aed9fe95c200. While the of_tuple function is clearly dubious and mostly used for compatiblity reasons, and thus had to be removed, I think that the to_tuple function is still useful as it allows to access each component of the declaration piecewise. Without it, some codes tend to get cluttered with useless projections here and there.
| | * | | Fix #4978: priorities of Equivalence instancesGravatar Matthieu Sozeau2016-08-17
| |/ / /
| * | | Fixing #3070 ("subst" taking properly into account chains of dependencies).Gravatar Hugo Herbelin2016-08-17
| | | |
| * | | Two protections against failures when printing evar_map.Gravatar Hugo Herbelin2016-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).Gravatar Hugo Herbelin2016-08-17
| | | |
| * | | A fix to dev/include.Gravatar Hugo Herbelin2016-08-17
| | | |
| | | * infoH: output via msg_* to make the XML protocol happyGravatar Enrico Tassi2016-08-17
| | | |
| * | | Removing dead unsafe debugging code in Constrintern.Gravatar Pierre-Marie Pédrot2016-08-16
| | | |
| | | * Output a break before a list only if there was an empty line (bug #4606).Gravatar Guillaume Melquiond2016-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.6Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \
| * \ \ \ Merge PR #237 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \ \
| * \ \ \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \ \ \ | | | |_|_|/ | | |/| | |
| * | | | | Efficiently generate the pretyping contexts.Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We used to recompute all fresh named contexts for evars before this patch in the push_rel_context_to_named_context function. This was incurring a linear penalty and a memory explosion due to the reallocation of many arrays. Now, we rather remember the context between evar creations by sharing it in the pretyping environment. This can be considered as a fix for bug #4964 even though we might do better.
| | | * \ \ \ Merge branch 'pr255' into v8.5 (bug #5015)Gravatar Guillaume Melquiond2016-08-16
| | | |\ \ \ \
| | | | * | | | Fix regression in Coqide's "forward one command" commandGravatar Xavier Leroy2016-08-14
| | | |/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".". In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed. I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
* | | | | | | Adding "Context.Named.Declaraton.of_rel" functionGravatar Matej Kosik2016-08-11
| | | | | | |
* | | | | | | CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" ↵Gravatar Matej Kosik2016-08-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | function
* | | | | | | CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" ↵Gravatar Matej Kosik2016-08-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | function
* | | | | | | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 04:30:18 +0000