aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-25Merge commit 'a799600' into v8.6Maxime Dénès
2016-10-25That Function is unable to create a Fixpoint equation is a user problem,Yves Bertot
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-24ssrmatching: fix interpretation of rpatternEnrico Tassi
2016-10-22Renamings to avoid confusion deprecating old namesMatthieu Sozeau
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
2016-10-18[pp] Use more convenient pp API in ssrmatchingEmilio Jesus Gallego Arias
2016-10-18[pp] Add tagging function to all low-level printing calls.Emilio Jesus Gallego Arias
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-17Fix bug #5023: JSON extraction doesn't generate "for xxx".Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-29Ncring_initial: avoid a notation overridingPierre Letouzey
2016-09-29Extraction: ignore some useless stuff about universesPierre Letouzey
2016-09-28Ring_theory: avoid overriding a few notationsPierre Letouzey
2016-09-28Adding interface files to Nsatz ML files.Pierre-Marie Pédrot
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-26Fast russian peasant exponentiation in Nsatz.Pierre-Marie Pédrot
2016-09-26Monomorphizing various uses of arrays in Nsatz.Pierre-Marie Pédrot
2016-09-26Partial fix for bug #5085: nsatz_compute stack overflows.Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-22Merge remote-tracking branch 'github/pr/283' into trunkMaxime Dénès
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-09-16Addressing OCaml compilation warnings.Hugo Herbelin
2016-09-16Make the Coq codebase independent from Ltac-related code.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
2016-09-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-07micromega : more robust generation of proof termsFrédéric Besson
2016-09-03Fixing what is probably a typo in Strict Proofs mode (#5062).Hugo Herbelin
2016-09-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-01Fixed Bug #5003 : more careful generalisation of dependent terms.Frédéric Besson
2016-08-31Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Frédéric Besson
2016-08-30plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...Frédéric Besson
2016-08-30micromega cache files are now hidden files (cf #4156)Frédéric Besson
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Matej Kosik
2016-08-30CLEANUP: using |> operator more consistentlyMatej Kosik
2016-08-29CLEANUP: taking advantage of "_ % _" operator to express function composition...Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:45:51 +0000