| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-20 | Remove dead code in library/lib.ml. | Maxime Dénès | |
| 2016-09-19 | Fix warning when using Variables at toplevel. | Maxime Dénès | |
| 2016-09-17 | Further "decide equality" tests on demand of Jason. | Hugo Herbelin | |
| 2016-09-16 | Addressing OCaml compilation warnings. | Hugo Herbelin | |
| One of them revealed a true bug. | |||
| 2016-09-16 | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin | |
| goal is under focus and which support returning a relevant output. | |||
| 2016-09-15 | 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 | |
| ~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. | |||
| 2016-09-15 | Continuing fix to #5078, taking also into account intropatterns. | Hugo Herbelin | |
| Getting closer from before when the bug was introduced + test. | |||
| 2016-09-15 | Typo. | Hugo Herbelin | |
| 2016-09-14 | 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-13 | 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 | |
| This way par:eauto and all:eato print the same debugging traecs | |||
| 2016-09-13 | stm: feedback forwarding has to be atomic | Enrico Tassi | |
| 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. | |||
| 2016-09-13 | feedback: provide a feeder that prints debug messages | Enrico Tassi | |
| 2016-09-12 | 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-11 | Add support for testing output mod timing changes | Jason Gross | |
| 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. | |||
| 2016-09-11 | Fix newlines in printout of LtacProf | Jason Gross | |
| Previously, newlines were missing if a node had no children. | |||
| 2016-09-11 | Revert the LtacProf tactic table header | Jason Gross | |
| 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.) | |||
| 2016-09-11 | Add a test for 4836 | Jason Gross | |
| This required improving the machinery of the test-suite Makefile to support -compile. | |||
| 2016-09-10 | Avoid putting a useless "toploop" directory in the ML search path if it does ↵ | Guillaume Melquiond | |
| not exist. | |||
| 2016-09-10 | Test for #5077. | Hugo Herbelin | |
| 2016-09-10 | Fixing #5077 (failure on typing a fixpoint with evars in its type). | Hugo Herbelin | |
| Typing.type_of was using conversion for types of fixpoints while it could have used unification. | |||
| 2016-09-09 | Updating .gitignore. | Hugo Herbelin | |
| 2016-09-09 | no-refold patch | Paul Steckler | |
| 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. | |||
| 2016-09-09 | 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 | |
| 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. | |||
| 2016-09-09 | Monomorphize a costly boolean equality operation. | Pierre-Marie Pédrot | |
| 2016-09-09 | Fix bug #4940: Tactic notation printing could be more informative. | Pierre-Marie Pédrot | |
| 2016-09-09 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-09 | Restore native compiler optimizations after they were broken by 9e2ee58. | Maxime Dénès | |
| The greatest danger of OCaml's polymorphic equality is that PMP can replace it with pointer equality at any time, be warned :) The lack of optimization may account for an exponential blow-up in size of the generated code, as well as worse runtime performance. | |||
| 2016-09-09 | Make it explicit when paths are added to the ML search paths. | Guillaume Melquiond | |
| When Mltop.add_rec_path was called to add paths to the loadpath, it was also adding the top directory to the mlpath. In particular, "theories" was added to the mlpath although it was explicitly marked "~with_ml:false". The "plugins" and "user-contribs" subdirectories were scanned twice, once for filling the loadpath and then for filling the mlpath. This patch adds an argument to Mltop.add_rec_path to explicitly control which paths from the loadpath are added to the mlpath (none, the top one, all of them). The "top" option was the single old behavior; the "none" option is used for "theories"; the "all" option is used to avoid duplicate scanning for "plugins" and "user-contribs". | |||
| 2016-09-09 | Update csdp cache. | Pierre-Marie Pédrot | |
| This was making the test-suite fail on machines where csdp was not installed. | |||
| 2016-09-09 | Fix bug #3920 for good after 44ada64. | Pierre-Marie Pédrot | |
| The previous commit did not apply the beta reduction for compatibility on the correct goal. We rather apply it on the first generated subgoal. This fixes the ergo contrib. | |||
| 2016-09-08 | Fix Bug #5073 : regression of micromega plugin | Frédéric Besson | |
| esprit d'escalier : is now also fixed for R | |||
| 2016-09-08 | Avoid canonizing the same paths over and over. | Guillaume Melquiond | |
| The number of path canonizations was quadratic in the number of potential plugin directories. This patch makes it linear; on a standard Coq tree, this brings the number of chdir and getcwd system calls from more than 1,000 down to about 200 at startup. This also fixes a bug where the Cd vernacular command could cause plugins to break since relative paths were used to locate them. | |||
| 2016-09-08 | Fix Bug #5073 : regression of micromega plugin | Frédéric Besson | |
| The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail. | |||
| 2016-09-08 | Merge PR #271 into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-07 | Fix a typo in the reference manual | Jason Gross | |
| 2016-09-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-07 | CoqIDE: Errors are sticky (fix #4368) | Enrico Tassi | |
| 2016-09-07 | Removing useless tactic compatibility layer in Rewrite. | Pierre-Marie Pédrot | |
| 2016-09-07 | STM: if_verbose on "Checking task ..." (fix #4058) | Enrico Tassi | |
| 2016-09-07 | ltacprof: rec-calls are coaleshed | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |