aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Patternops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
| | | | | | | 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.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ | | | | | | | | | Was PR#319: More error tagging, try to fix bug 5135
| * \ Merge commit 'a799600' into v8.6Gravatar Maxime Dénès2016-10-25
| |\ \ | | | | | | | | | | | | Was PR#334: Fix bug 5031 : should not be an anomaly
| | * | That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
| | | | | | | | | | | | | | | | not an anomaly
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | |
| * | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
| |/ /
* | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
| | | | | | | | | | | | | | | | | | | | | 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
| | * [pp] Use more convenient pp API in ssrmatchingGravatar Emilio Jesus Gallego Arias2016-10-18
| | |
| | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/ | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Fix bug #5023: JSON extraction doesn't generate "for xxx".Gravatar Pierre-Marie Pédrot2016-10-17
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Ncring_initial: avoid a notation overridingGravatar Pierre Letouzey2016-09-29
| |
| * Extraction: ignore some useless stuff about universesGravatar Pierre Letouzey2016-09-29
| |
| * Ring_theory: avoid overriding a few notationsGravatar Pierre Letouzey2016-09-28
| |
| * Adding interface files to Nsatz ML files.Gravatar Pierre-Marie Pédrot2016-09-28
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
| * Fast russian peasant exponentiation in Nsatz.Gravatar Pierre-Marie Pédrot2016-09-26
| |
| * Monomorphizing various uses of arrays in Nsatz.Gravatar Pierre-Marie Pédrot2016-09-26
| |
| * Partial fix for bug #5085: nsatz_compute stack overflows.Gravatar Pierre-Marie Pédrot2016-09-26
| | | | | | | | | | 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.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
| | | | | | | | | | | | | | | | | | 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.
* | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \ | | | | | | | | | Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
* | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | | | | | | | | | | | | | | 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.
| * | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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".
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
| | | | | | | | One of them revealed a true bug.
* | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
| | |
| * | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ | |/ / |/| / | |/
| * Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
| | | | | | | | esprit d'escalier : is now also fixed for R
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
| | * Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
| | | | | | | | | | | | | | | The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ | | |/ | |/|
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-07
| |\ \
| * | | micromega : more robust generation of proof termsGravatar Frédéric Besson2016-09-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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)
| | * | Fixing what is probably a typo in Strict Proofs mode (#5062).Gravatar Hugo Herbelin2016-09-03
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 14:33:39 +0000