| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fast russian peasant exponentiation in Nsatz. |  Pierre-Marie Pédrot | 2016-09-26 |
| | | |||
| * | Monomorphizing various uses of arrays in Nsatz. | Pierre-Marie Pédrot | 2016-09-26 |
| | | |||
| * | Partial fix for bug #5085: nsatz_compute stack overflows. | Pierre-Marie Pédrot | 2016-09-26 |
| | | | | | | This fixes the stack overflow part of the bug, even if the tactic is still quite slow. The offending functions have been written in a tail-recursive way. | ||
| * | Fix bug #5093: typeclasses eauto depth arg does not accept a var. | Pierre-Marie Pédrot | 2016-09-26 |
| | | |||
| * | Fix bug #5090: Effect of -Q depends on coqtop's current directory. | Pierre-Marie Pédrot | 2016-09-25 |
| | | | | | | | | This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It seems that the original motivation was to deactivate a warning when overriding the default loadpath binding of the current directory, but in the end it made it non-overridable. | ||
| * | The coqtop options -Q and -R do not affect the ML loadpath anymore. | Pierre-Marie Pédrot | 2016-09-25 |
| | | | | | | | It seems that such options were adding the considered path to the ML loadpath as well, which is not what is documented, and does not provide an atomic way to manipulate Coq loadpaths. | ||
| * | Moving "move" in the new proof engine. |  Hugo Herbelin | 2016-09-24 |
| | | |||
| * | Adding a test for bug #5096. | Pierre-Marie Pédrot | 2016-09-24 |
| | | |||
| * | Fix bug #5096: [vm_compute] is exponentially slower than [native_compute]. | Pierre-Marie Pédrot | 2016-09-23 |
| | | | | | | | | | | | | | The fix is essentially a revert of f22ad60 that introduced the use of the pretyper version of whd_all instead of the one from the kernel. The exact cause of slowness of the pretyper version is still to be investigated, but it is believed that it is due to a call-by-name strategy, to compare with call-by-need in the kernel. Note that there is still something fishy in presence of evars. Technically vm_compute does not handle them, but if this comes to be the case, it might be worthwile to use an evar-aware variant of whd_all. | ||
| * | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-23 |
| |\ | |||
| * | | coqc -o now places .glob file near .vo file |  Enrico Tassi | 2016-09-22 |
| | | | | | | | | | | | All compilation (by)products are placed where -o specifies. Used to be the case for .vo, .vio, .aux but not .glob | ||
| * | | typos | Enrico Tassi | 2016-09-22 |
| | | | |||
| | * | Fixing #5095 (non relevant too strict test in let-in abstraction). | Hugo Herbelin | 2016-09-22 |
| | | | |||
| * | | Fix description of change in intro semantics. |  Maxime Dénès | 2016-09-21 |
| | | | |||
| * | | Remove dead code in library/lib.ml. | Maxime Dénès | 2016-09-20 |
| | | | |||
| | * | Replace { command ; } with ( command ) |  Erik Martin-Dorel | 2016-09-19 |
| | | | | | | | | | | | as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output. | ||
| | * | Fix typos in RefMan-uti.tex. | Erik Martin-Dorel | 2016-09-19 |
| | | | | | | | | | | | | | - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace. | ||
| * | | Fix warning when using Variables at toplevel. | Maxime Dénès | 2016-09-19 |
| | | | |||
| * | | Further "decide equality" tests on demand of Jason. | Hugo Herbelin | 2016-09-17 |
| | | | |||
| * | | Addressing OCaml compilation warnings. | Hugo Herbelin | 2016-09-16 |
| | | | | | | | | | One of them revealed a true bug. | ||
| * | | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin | 2016-09-16 |
| | | | | | | | | | goal is under focus and which support returning a relevant output. | ||
| * | | Added a test file for contradiction. | Hugo Herbelin | 2016-09-15 |
| | | | |||
| * | | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵ | Hugo Herbelin | 2016-09-15 |
| | | | | | | | | | | | | | | | | | | | | | ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5. | ||
| * | | Continuing fix to #5078, taking also into account intropatterns. | Hugo Herbelin | 2016-09-15 |
| | | | | | | | | | Getting closer from before when the bug was introduced + test. | ||
| * | | Typo. | Hugo Herbelin | 2016-09-15 |
| | | | |||
| * | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-14 |
| |\| | |||
| | * | Fixing test-suite after commit 43104a0b. | Pierre-Marie Pédrot | 2016-09-14 |
| | | | |||
| * | | Fixing #5078 (wrong detection of evaluable local hypotheses). | Hugo Herbelin | 2016-09-13 |
| | | | |||
| * | | LtacProp: fix reset_profile (fix #5079) | Enrico Tassi | 2016-09-13 |
| | | | |||
| * | | test-suite/output-modulo-time made more robust | Enrico Tassi | 2016-09-13 |
| | | | |||
| * | | AsyncTaskQueue: annotate debug feedback messages with worker id | Enrico Tassi | 2016-09-13 |
| | | | |||
| * | | CoqIDE: push to message win feedback Message(Debug,Info,Notice) | Enrico Tassi | 2016-09-13 |
| | | | |||
| * | | coqc: print debug feedback coming from workers | Enrico Tassi | 2016-09-13 |
| | | | | | | | | | This way par:eauto and all:eato print the same debugging traecs | ||
| * | | stm: feedback forwarding has to be atomic | Enrico Tassi | 2016-09-13 |
| | | | | | | | | | | | | | I think that a better place for the mutex would be the printing routine, but I still hope we will get rid of threads in favor of coroutines. So I keep all mutexes in Stm. | ||
| * | | feedback: provide a feeder that prints debug messages | Enrico Tassi | 2016-09-13 |
| | | | |||
| | * | Fixing a recursive notation bug raised on coq-club on Sep 12, 2016. | Hugo Herbelin | 2016-09-12 |
| | | | |||
| * | | Refolding: disable in 8.4 compat file, document |  Matthieu Sozeau | 2016-09-12 |
| | | | |||
| * | | Merge remote-tracking branch 'github-coq/pr/249' into v8.6 | Matthieu Sozeau | 2016-09-12 |
| |\ \ | |||
| * | | | Add support for testing output mod timing changes |  Jason Gross | 2016-09-11 |
| | | | | | | | | | | | | | | | | | | | | | | | | | Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip numbers of seconds and to strip percentages. (This can potentially be extended later.) Add a test-suite file to make sure that LtacProf outputs some table. | ||
| * | | | Fix newlines in printout of LtacProf |  Jason Gross | 2016-09-11 |
| | | | | | | | | | | | | | Previously, newlines were missing if a node had no children. | ||
| * | | | Revert the LtacProf tactic table header | Jason Gross | 2016-09-11 |
| | | | | | | | | | | | | | This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read. (This way, the alignment of the headers matches the alignment of the entries.) | ||
| * | | | Add a test for 4836 | Jason Gross | 2016-09-11 |
| | | | | | | | | | | | | | | | | This required improving the machinery of the test-suite Makefile to support -compile. | ||
| * | | | Avoid putting a useless "toploop" directory in the ML search path if it does ↵ |  Guillaume Melquiond | 2016-09-10 |
| | | | | | | | | | | | | | not exist. | ||
| | | * | Test for #5077. | Hugo Herbelin | 2016-09-10 |
| | | | | |||
| | | * | Fixing #5077 (failure on typing a fixpoint with evars in its type). | Hugo Herbelin | 2016-09-10 |
| | | | | | | | | | | | | | | | | Typing.type_of was using conversion for types of fixpoints while it could have used unification. | ||
| * | | | Updating .gitignore. | Hugo Herbelin | 2016-09-09 |
| | | | | |||
| | * | | no-refold patch |  Paul Steckler | 2016-09-09 |
| | | | | | | | | | | | | | | | | | | | Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5. | ||
| * | | | Fix output test-suite after commit 0d3c319. | Pierre-Marie Pédrot | 2016-09-09 |
| | | | | |||
| * | | | Fast path in Clenvtac.clenv_refine typeclass resolution. | Pierre-Marie Pédrot | 2016-09-09 |
| | | | | | | | | | | | | | | | | | | | This legacy function is still used by destruct, and is a hotspot in various examples from the wild. We hijack the check from Typeclass and perform a double check at once not to mark unresolvable evars in vain a lot. | ||
| * | | | Monomorphize a costly boolean equality operation. | Pierre-Marie Pédrot | 2016-09-09 |
| | | | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |