aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-08-29Fix tagging of notations.Pierre-Marie Pédrot
We only tag the non-whitespace substrings, rather than the whole terminal token.
2016-08-29Fix inefficiency in CoqIDE display of tagged text.Pierre-Marie Pédrot
The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function.
2016-08-29Send Dependency feedback only if file not already loaded.Maxime Dénès
2016-08-28Fix bug #4750: Change format of inconsistent assumptions message.Pierre-Marie Pédrot
We now print the file responsible for the incompatibility in require error messages.
2016-08-28Fix bug #4764: Syntactic notation externalization breaks.Pierre-Marie Pédrot
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-08-25FIX: Coq versionMatej Kosik
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-24Properly compute types for assumed section variables (bug #5035).Guillaume Melquiond
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
2016-08-24Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Pierre-Marie Pédrot
2016-08-24Merge PR #258: "Fix newline issues" into v8.6Pierre-Marie Pédrot
2016-08-23Fix bug #4914: LtacProf printout has too many newlines.Pierre-Marie Pédrot
2016-08-23Arguments: give / after last ! error detection fixedEnrico Tassi
2016-08-23fix get_host_port error message (#4724)Enrico Tassi
2016-08-23update Proof General URLPaul Steckler
2016-08-23Fix bug #4904: [Import] does not load intermediately unqualified names of ↵Pierre-Marie Pédrot
aliases.
2016-08-22Fast path for set operations.Pierre-Marie Pédrot
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.
2016-08-22Merge remote-tracking branch 'github/pr/261' into v8.6Maxime Dénès
Was PR#261: Use a better data structure for VM compilation of free vars.
2016-08-22Use a better data structure for VM compilation of free vars.Pierre-Marie Pédrot
This fixes #3450 and probably provides a huge speed-up to many instances.
2016-08-22Pushing error backtrace in unification reraise.Pierre-Marie Pédrot
2016-08-21Documenting "Set Structural Injection".Hugo Herbelin
2016-08-21Do not recompute the whole evar naming environment in GProd intepretation.Pierre-Marie Pédrot
2016-08-21Short path for Pretyping.ltac_interp_name_env.Pierre-Marie Pédrot
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!
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-19[pp] Fix bug 4842 (Time prints in multiple lines)Emilio Jesus Gallego Arias
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.
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-19[pp] Fix newline issues.Emilio Jesus Gallego Arias
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
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-17Fix #4978: priorities of Equivalence instancesMatthieu Sozeau
2016-08-17Fixing #3070 ("subst" taking properly into account chains of dependencies).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 00:21:55 +0000