aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2016-10-17Fix bug #5023: JSON extraction doesn't generate "for xxx".Pierre-Marie Pédrot
2016-09-29Extraction: ignore some useless stuff about universesPierre Letouzey
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
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-23Extraction/Projections: Fix bug #4710Matthieu Sozeau
2016-05-20Extraction: code cleanup in CommonPierre Letouzey
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Fix Haskell extraction for terms over 45 characters longNickolai Zeldovich
2016-05-04Handle primitive projections inside types when extracting (bug #4616).Guillaume Melquiond
2016-05-04Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...Pierre Letouzey
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-04-09Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vNickolai Zeldovich
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-02-19Fix Haskell extraction for terms over 45 characters longNickolai Zeldovich
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-05Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-04Extraction: msg_notice instead of msg_info.Pierre Courtieu
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-16Extraction: slightly better heuristic for Obj.magic simplificationsPierre Letouzey
2015-12-16Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsPierre Letouzey
2015-12-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
2015-12-15Extraction: fix a few little glitches with my last commit (replacing unused v...Pierre Letouzey
2015-12-15Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Pierre Letouzey
2015-12-14Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Pierre Letouzey
2015-12-14Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Pierre Letouzey
2015-12-14Extraction: cosmetically avoid generating spaces on empty linesPierre Letouzey
2015-12-14Extraction: also get rid of explicit '\n' for haskellPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:10:44 +0000