aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-09-16Make 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-15Documenting API changes.Pierre-Marie Pédrot
2016-09-15Moving Tacexpr to ltac/ folder.Pierre-Marie Pédrot
2016-09-15Made Ppanotation Ltac-agnostic.Pierre-Marie Pédrot
2016-09-15Added a test file for contradiction.Hugo Herbelin
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-15Extending "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-15Continuing fix to #5078, taking also into account intropatterns.Hugo Herbelin
Getting closer from before when the bug was introduced + test.
2016-09-15Typo.Hugo Herbelin
2016-09-15Moving Tactic_matching to ltac/ folder.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-15Moving Ltac printers to ltac/ folder.Pierre-Marie Pédrot
2016-09-15Generalizing the notion of constr substitution to generic arguments.Pierre-Marie Pédrot
This removes a dependency on wit_tactic in Constrintern.
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-09-14Moving the tactic-in-term extension from G_constr to G_ltac.Pierre-Marie Pédrot
2016-09-14Fix CAMLP4 compilation.Pierre-Marie Pédrot
2016-09-14Allowing to extend the Print Grammar command generically.Pierre-Marie Pédrot
We also move the Ltac-specific grammar to its folder.
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-14Fixing test-suite after commit 43104a0b.Pierre-Marie Pédrot
2016-09-13Fixing #5078 (wrong detection of evaluable local hypotheses).Hugo Herbelin
2016-09-13LtacProp: fix reset_profile (fix #5079)Enrico Tassi
2016-09-13test-suite/output-modulo-time made more robustEnrico Tassi
2016-09-13AsyncTaskQueue: annotate debug feedback messages with worker idEnrico Tassi
2016-09-13CoqIDE: push to message win feedback Message(Debug,Info,Notice)Enrico Tassi
2016-09-13coqc: print debug feedback coming from workersEnrico Tassi
This way par:eauto and all:eato print the same debugging traecs
2016-09-13stm: feedback forwarding has to be atomicEnrico 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-13feedback: provide a feeder that prints debug messagesEnrico Tassi
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-09-12Refolding: disable in 8.4 compat file, documentMatthieu Sozeau
2016-09-12Merge remote-tracking branch 'github-coq/pr/249' into v8.6Matthieu Sozeau
2016-09-11Add support for testing output mod timing changesJason 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-11Fix newlines in printout of LtacProfJason Gross
Previously, newlines were missing if a node had no children.
2016-09-11Revert the LtacProf tactic table headerJason 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-11Add a test for 4836Jason Gross
This required improving the machinery of the test-suite Makefile to support -compile.
2016-09-11Move Ltac-specific components from G_proofs to G_ltac.Pierre-Marie Pédrot
2016-09-10Avoid putting a useless "toploop" directory in the ML search path if it does ↵Guillaume Melquiond
not exist.
2016-09-10Test for #5077.Hugo Herbelin
2016-09-10Fixing #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-09Updating .gitignore.Hugo Herbelin
2016-09-09no-refold patchPaul 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-09Merge PR #274.Pierre-Marie Pédrot
2016-09-09Fix output test-suite after commit 0d3c319.Pierre-Marie Pédrot
2016-09-09Fast 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-09Propagate 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-09Monomorphize a costly boolean equality operation.Pierre-Marie Pédrot
2016-09-09Fix bug #4940: Tactic notation printing could be more informative.Pierre-Marie Pédrot
2016-09-09Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-09-09Restore 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 09:08:20 +0000