aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2017-02-08Merge PR#393: Replace Typeops with Fast_typeopsMaxime Dénès
2017-02-07Revert "Extraction: avoid deprecated functions of module String"Pierre Letouzey
2017-02-07Extraction cosmetic: no whitespaces in printing empty modulesPierre Letouzey
2017-02-07Extraction: remove the "print to devnull" hack now that pp isn't lazy anymorePierre Letouzey
2017-02-07Extraction: avoid deprecated functions of module StringPierre Letouzey
2017-02-07Extraction: simplify the generated code for difficult name conflictsPierre Letouzey
2017-02-07Extraction : get_duplicates (via option) instead of check_duplicates (via Not...Pierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-01-28Remove useless commentsGaetan Gilbert
2017-01-19Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-12Extend Fast_typeops to be a replacement for TypeopsGaetan Gilbert
2016-12-07ssrmatching: fix iter_constr_LR iterator wrt ProjEnrico Tassi
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-05ssrmatching: handle primite projections (fix: #5247)Enrico Tassi
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 15:31:26 +0000