aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Micromega: removing a constant preventing micromega to be loaded before Logic.v.Gravatar Hugo Herbelin2017-03-09
* Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
|\
* | Revert "Add empty ltac_plugin file for forward compatibility."Gravatar Maxime Dénès2017-02-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
|\ \
* | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
* | | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
* | | Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
|\ \ \
* | | | Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
* | | | Extraction cosmetic: no whitespaces in printing empty modulesGravatar Pierre Letouzey2017-02-07
* | | | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymoreGravatar Pierre Letouzey2017-02-07
* | | | Extraction: avoid deprecated functions of module StringGravatar Pierre Letouzey2017-02-07
* | | | Extraction: simplify the generated code for difficult name conflictsGravatar Pierre Letouzey2017-02-07
* | | | Extraction : get_duplicates (via option) instead of check_duplicates (via Not...Gravatar Pierre Letouzey2017-02-07
* | | | Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| |_|/ |/| |
| | * Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| * | Remove useless commentsGravatar Gaetan Gilbert2017-01-28
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ | | |/ | |/|
| | * Extend Fast_typeops to be a replacement for TypeopsGravatar Gaetan Gilbert2016-12-12
| |/ |/|
| * ssrmatching: fix iter_constr_LR iterator wrt ProjGravatar Enrico Tassi2016-12-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\|
| * ssrmatching: handle primite projections (fix: #5247)Gravatar Enrico Tassi2016-12-05
| * Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-12-02
* | 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