aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2017-01-19Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-07ssrmatching: fix iter_constr_LR iterator wrt ProjEnrico Tassi
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-05ssrmatching: handle primite projections (fix: #5247)Enrico Tassi
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
Was PR#331: Solve_constraints and Set Use Unification Heuristics
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there.
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
Was PR#319: More error tagging, try to fix bug 5135
2016-10-25Merge commit 'a799600' into v8.6Maxime Dénès
Was PR#334: Fix bug 5031 : should not be an anomaly
2016-10-25That Function is unable to create a Fixpoint equation is a user problem,Yves Bertot
not an anomaly
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-24ssrmatching: fix interpretation of rpatternEnrico Tassi
2016-10-22Renamings to avoid confusion deprecating old namesMatthieu Sozeau
reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
The word "increment" is more appropriate in this case than "lifting". The world "lifting", in computer science, usually denotes something else: https://en.wikipedia.org/wiki/Lambda_lifting
2016-10-18[pp] Use more convenient pp API in ssrmatchingEmilio Jesus Gallego Arias
2016-10-18[pp] Add tagging function to all low-level printing calls.Emilio Jesus Gallego Arias
The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases.
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-17Fix bug #5023: JSON extraction doesn't generate "for xxx".Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-29Ncring_initial: avoid a notation overridingPierre Letouzey
2016-09-29Extraction: ignore some useless stuff about universesPierre Letouzey
2016-09-28Ring_theory: avoid overriding a few notationsPierre Letouzey
2016-09-28Adding interface files to Nsatz ML files.Pierre-Marie Pédrot
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-26Fast russian peasant exponentiation in Nsatz.Pierre-Marie Pédrot
2016-09-26Monomorphizing various uses of arrays in Nsatz.Pierre-Marie Pédrot
2016-09-26Partial fix for bug #5085: nsatz_compute stack overflows.Pierre-Marie Pédrot
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.
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
2016-09-22Merge remote-tracking branch 'github/pr/283' into trunkMaxime Dénès
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic".
2016-09-16Addressing OCaml compilation warnings.Hugo Herbelin
One of them revealed a true bug.
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-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
esprit d'escalier : is now also fixed for R
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-09-08Fix Bug #5073 : regression of micromega pluginFré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-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-07micromega : more robust generation of proof termsFrédéric Besson
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
2016-09-03Fixing what is probably a typo in Strict Proofs mode (#5062).Hugo Herbelin
2016-09-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 19:11:29 +0000