| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-14 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 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-11 | Move Ltac-specific components from G_proofs to G_ltac. | Pierre-Marie Pédrot | |
| 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 | Merge PR #274. | Pierre-Marie Pédrot | |
| 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 | Propagate location info on pattern match compilation. | Emilio Jesus Gallego Arias | |
| This is a follow-up to #244 and corrects a minor bug introduced by the patch. | |||
| 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 | Tracking careless uses of slow name lookup. | 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 | Removing the now useless field env_named_val from named_context_val. | Pierre-Marie Pédrot | |
| This field was only used by the VM before, but since the previous patches, this part of the code relies on the map instead. | |||
| 2016-09-09 | More efficient implementation of map_named_val. | Pierre-Marie Pédrot | |
| 2016-09-09 | Fast access environment in CClosure. | Pierre-Marie Pédrot | |
| 2016-09-09 | Tentative fast-access named env | Pierre-Marie Pédrot | |
| 2016-09-09 | Packing the named_context_val in a proper record and marking it private. | Pierre-Marie Pédrot | |
| 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 | A proposal for recommended uniformity of style in programming Coq. | Hugo Herbelin | |
| Starting listing some recommendations in using the API. | |||
| 2016-09-09 | Removing the last uses of Pptactic in the lower layers. | Pierre-Marie Pédrot | |
| 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 | Unplugging Pptactic from Ppvernac. | Pierre-Marie Pédrot | |
| 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 | Making Proof_global terminator generic in external tactics. | Pierre-Marie Pédrot | |
| 2016-09-08 | Making Hints generic in the use of external tactics. | Pierre-Marie Pédrot | |
| 2016-09-08 | Unplugging Tacexpr in several interface files. | Pierre-Marie Pédrot | |
| 2016-09-08 | Making Vernacexpr independent from Tacexpr. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |