aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-23Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
2017-03-21[extraction] Flush formatters at end of output.Emilio Jesus Gallego Arias
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2017-03-21[pp] Prepare for serialization, remove opaque glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove `Pp.stras`.Emilio Jesus Gallego Arias
2017-03-14[safe-string] plugins/extractionEmilio Jesus Gallego Arias
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
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-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-01-28Remove useless commentsGaetan Gilbert
2016-12-12Extend Fast_typeops to be a replacement for TypeopsGaetan Gilbert
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
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-29Extraction: ignore some useless stuff about universesPierre Letouzey
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-10Make it a bit more obvious when variables are of type unit.Guillaume Melquiond
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-23Fix typo.Guillaume Melquiond
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 21:43:43 +0000