aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-08-24CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionMatej Kosik
2016-08-24CLEANUP: removing superfluous (module) qualifiersMatej Kosik
2016-08-24CLEANUP: removing unnecessary variable bindingMatej Kosik
2016-08-24Changing the definition of the "Lib.variable.info" type to enable us to do ↵Matej Kosik
more cleanups
2016-08-24Merging a branch that adds "Context.Named.Declaration.to_rel" function.Matej Kosik
2016-08-24Adding "Context.Named.Declaration.to_rel" functionMatej Kosik
2016-08-21Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-20More standard naming for the Imparg.with_implicits function.Pierre-Marie Pédrot
2016-08-20Fixing a bug in the presence of let-in while inferring the return clause.Hugo Herbelin
2016-08-20Fixing an anomaly in printing a unification error message.Hugo Herbelin
2016-08-19Test file for bug #4187.Pierre-Marie Pédrot
2016-08-19Fix performance bug: do not compute implicits of abstracted lemmas.Pierre-Marie Pédrot
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.
2016-08-19Removing dead code in Impargs.Pierre-Marie Pédrot
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-08-19Moving Taccoerce to ltac/ folder.Pierre-Marie Pédrot
This was an overlook. There was no reason to let it in the tactics/ folder, as is was semantically part of the Ltac implementation.
2016-08-19Remove extraneous dot in error message (bug #4832).Guillaume Melquiond
2016-08-19Fix anomaly on user-inputted projection name (bug #5029).Guillaume Melquiond
2016-08-18Merge remote-tracking branch 'github/bug4978' into v8.6Matthieu Sozeau
2016-08-18Merge remote-tracking branch 'github/bug4188' into v8.6Matthieu Sozeau
2016-08-18Fix incorrect glob data for module symbols (bug #2336).Guillaume Melquiond
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.
2016-08-18Fix an occurrence of deprecated eqn syntax in stdlib.Maxime Dénès
2016-08-18Fix bug #4939: LtacProf prints tactic notations weirdly.Pierre-Marie Pédrot
2016-08-18Adding a test for bug #4653.Pierre-Marie Pédrot
2016-08-18Merge PR #256 into v8.6Pierre-Marie Pédrot
2016-08-17In docs, fix command to reset Ltac profilingPaul Steckler
2016-08-17Fix setoid_rewrite to raise proper errorsMatthieu Sozeau
when the rewrite lemma doesn't typecheck or does not correspond to a relation.
2016-08-17Fixing #5001 (metas not cleaned properly in clenv_refine_in).Hugo Herbelin
Fixing by copying what Matthieu did for Clenvtac.clenv_refine.
2016-08-17Fixing CHANGES.Hugo Herbelin
Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section.
2016-08-17Documenting fix of #3070 (subst and chain of dependencies).Hugo Herbelin
2016-08-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-17Revert "CLEANUP: removing the definition of the ↵Pierre-Marie Pédrot
"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.
2016-08-17Fix #4978: priorities of Equivalence instancesMatthieu Sozeau
2016-08-17Fixing #3070 ("subst" taking properly into account chains of dependencies).Hugo Herbelin
2016-08-17Two protections against failures when printing evar_map.Hugo Herbelin
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).
2016-08-17Fixing printing in debugger (no global env in debugger).Hugo Herbelin
2016-08-17A fix to dev/include.Hugo Herbelin
2016-08-17infoH: output via msg_* to make the XML protocol happyEnrico Tassi
2016-08-16Removing dead unsafe debugging code in Constrintern.Pierre-Marie Pédrot
2016-08-16Output a break before a list only if there was an empty line (bug #4606).Guillaume Melquiond
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.
2016-08-16Merge PR #250 into v8.6Pierre-Marie Pédrot
2016-08-16Merge PR #237 into v8.6Pierre-Marie Pédrot
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-16Efficiently generate the pretyping contexts.Pierre-Marie Pédrot
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.
2016-08-16Merge branch 'pr255' into v8.5 (bug #5015)Guillaume Melquiond
2016-08-14Fix regression in Coqide's "forward one command" commandXavier Leroy
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".
2016-08-11Adding "Context.Named.Declaraton.of_rel" functionMatej Kosik
2016-08-11CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" ↵Matej Kosik
function
2016-08-11CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" ↵Matej Kosik
function
2016-08-11CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 22:22:27 +0000