| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-19 | Adding an "extensionality in H" tactic which applies functional | Hugo Herbelin | |
| extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples. | |||
| 2016-09-16 | Make the Coq codebase independent from Ltac-related code. | Pierre-Marie Pédrot | |
| We untangle many dependencies on Ltac datastructures and modules from the lower strata, resulting in a self-contained ltac/ folder. While not a plugin yet, the change is now very easy to perform. The main API changes have been documented in the dev/doc/changes file. The patches are quite rough, and it may be the case that some parts of the code can migrate back from ltac/ to a core folder. This should be decided on a case-by-case basis, according to a more long-term consideration of what is exactly Ltac-dependent and whatnot. | |||
| 2016-09-15 | Documenting API changes. | Pierre-Marie Pédrot | |
| 2016-09-15 | Moving Tacexpr to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Made Ppanotation Ltac-agnostic. | Pierre-Marie Pédrot | |
| 2016-09-15 | Untangling Tacexpr from lower strata. | Pierre-Marie Pédrot | |
| 2016-09-15 | Moving Tactic_matching to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Moving Ltac-specific generic arguments to their own file in the ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Moving Ltac printers to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Generalizing the notion of constr substitution to generic arguments. | Pierre-Marie Pédrot | |
| This removes a dependency on wit_tactic in Constrintern. | |||
| 2016-09-14 | Moving Ltac-specific parsing API to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-14 | Moving the tactic-in-term extension from G_constr to G_ltac. | Pierre-Marie Pédrot | |
| 2016-09-14 | Fix CAMLP4 compilation. | Pierre-Marie Pédrot | |
| 2016-09-14 | Allowing to extend the Print Grammar command generically. | Pierre-Marie Pédrot | |
| We also move the Ltac-specific grammar to its folder. | |||
| 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 | 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 | 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |