aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Lazily load constants in micromega (bug #5134).Gravatar Guillaume Melquiond2016-11-24
* Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
|\
* \ 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
* | | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
|/ / /
| | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| |/ |/|
| * [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
|/
* Fix bug #5023: JSON extraction doesn't generate "for xxx".Gravatar Pierre-Marie Pédrot2016-10-17
* 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
* 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
* Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
* Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
* 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.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
* | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
* | Reduce warning noise when compiling the standard library.Gravatar Guillaume Melquiond2016-08-09
* | Fix bug #4923: Warning: appcontext is deprecated.Gravatar Pierre-Marie Pédrot2016-07-18
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-13
|\|
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\ \
| | * improved complexity in nsatzGravatar thery2016-07-06
| | * Bug Fixes : 4851 4858 4880 for nsatzGravatar thery2016-07-06
| |/
* | Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Gravatar Maxime Dénès2016-07-05
| * Bug fix : variable capture in ltac code of NsatzGravatar thery2016-07-05
* | Merge remote-tracking branch 'github/pr/229' into trunkGravatar Maxime Dénès2016-07-04
|\ \
| | * congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| | * congruence: remove casts of indexed termsGravatar Matthieu Sozeau2016-07-04
| | * congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
* | | rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* | | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* | | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* | | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| * | Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2016-06-29
|/ /
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDGravatar Pierre Letouzey2016-06-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 18:14:38 +0000