aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* 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
* | 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
* | | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | | CLEANUP: taking advantage of "_ % _" operator to express function composition...Gravatar Matej Kosik2016-08-29
* | | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
* | | | CLEANUP: removing unnecessary variable bindingGravatar Matej Kosik2016-08-24
| | | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |_|/ |/| |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\| |
* | | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
| * | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 23:57:56 +0000