aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
...
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Lazily load constants in micromega (bug #5134).Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
* | | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* | | 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
| |\ \
| * \ \ Merge commit 'a799600' into v8.6Gravatar Maxime Dénès2016-10-25
| |\ \ \
| | * | | That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | | |
| * | | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
| |/ / /
| | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |/ | |/|
* | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
| | * [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
| |/
* | 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
* | 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
* | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \
* | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| * | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ /
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \
| * | 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
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
| | * Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
* | | 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
| | * | Fixing what is probably a typo in Strict Proofs mode (#5062).Gravatar Hugo Herbelin2016-09-03
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
| |\| |
| * | | Fixed Bug #5003 : more careful generalisation of dependent terms.Gravatar Frédéric Besson2016-09-01
| * | | Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Gravatar Frédéric Besson2016-08-31
| * | | plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...Gravatar Frédéric Besson2016-08-30
| | * | micromega cache files are now hidden files (cf #4156)Gravatar Frédéric Besson2016-08-30
* | | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30