aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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 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-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
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-16Removing dead unsafe debugging code in Constrintern.Pierre-Marie Pédrot
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-11Do not assume the "TERM" environment variable is always set (bug #5007).Guillaume Melquiond
2016-08-11Use the "md5" command on OpenBSD (bug #5008).Guillaume Melquiond
2016-08-10Make code a bit clearer by removing optional argument.Guillaume Melquiond
2016-08-10Remove unused optional "predicative" argument.Guillaume Melquiond
2016-08-10Make it a bit more obvious when variables are of type unit.Guillaume Melquiond
2016-08-09Reduce warning noise when compiling the standard library.Guillaume Melquiond
2016-08-09Make List.map_filter(_i) tail-recursive.Guillaume Melquiond
While the performance gain should go unnoticed in most cases, in some degenerate situations, e.g. the evar-stressing test-case of bug #4964, this commit speeds up coq by 10% since most of the time is spent scanning long lists with most of the elements filtered out. Note that this commit also changes the scanning order to front-to-back, which is a bit less surprising (though no code should ever depend on the scanning order).
2016-08-07Fix #5000: Document the native compiler soundness bug due to Unicode mangling.Pierre-Marie Pédrot
2016-08-06Using a dedicated kind of substitutions in evar name generation.Pierre-Marie Pédrot
This saves a quadratic allocation by replacing arrays with maps.
2016-08-05Using the extended contexts in pretyping.Pierre-Marie Pédrot
In addition to sharing, we also delay the computation of the environment in a by-need fashion.
2016-08-04Use sets instead of lists for names to avoid in evar generation.Pierre-Marie Pédrot
2016-08-04Simplifying code in evar generation.Pierre-Marie Pédrot
We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences.
2016-08-04Exporting the renaming API for evar declaration.Pierre-Marie Pédrot
2016-08-04Embedding the pretyping environment in a dummy record.Pierre-Marie Pédrot
2016-08-04Fix documentation typo (bug #4994).Guillaume Melquiond
2016-07-29Fix bug #4673: regression in setoid_rewrite.Matthieu Sozeau
Modulo delta for types should be fully transparent.
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Update CHANGES about #3886 bugfixMatthieu Sozeau
2016-07-29Fix bug #3886, generation of obligations of fixesMatthieu Sozeau
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-29COMMENT: moving misplaced comment where it belongsMatej Kosik
2016-07-26Adding a flag in CoqIDE to configure UNIX/Windows line ending.Pierre-Marie Pédrot
Fixes both bugs #4924 and #4437.
2016-07-26restore compatibility with gallium's camlp4 (broken by commit 8e07227c)Pierre Letouzey
Apparently, in camlp4 (unlike camlp5) : - Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]" produces a kwd of type token instead of string (which sounds reasonable ?). For now, I've replaced kwd by the explicit strings. Not so nice, but works with both camlp4 and camlp5 - A quotation of the form "let obj = ... in bar; baz" is not interpreted in the usual OCaml way, but rather as "(let obj = ... in bar); baz". Let's use instead "let obj = ... in let () = bar in baz", which works fine.
2016-07-26Update CHANGES about critical bugfix and othersMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 00:44:12 +0000