aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/table.mli
AgeCommit message (Expand)Author
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-06-18Remove reference name type.Maxime Dénès
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-10-04Extraction : minor support stuff for the new Extraction Compute pluginPierre Letouzey
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2015-12-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-04-09Add extraction to JSON.Nickolai Zeldovich
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: minor tweaks to ease ongoing experiments about LambdaPierre Letouzey
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-05-12Use the Hook module here and there.ppedrot
2013-02-19Dir_path --> DirPathletouzey
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-08Updating headers.herbelin
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-08-25Extraction: allow extraction of records with anonymous fields (fix #2555)letouzey
2011-07-04Set Extraction KeepSingleton: an option for not decapsulating singleton typesletouzey
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2011-04-15Extraction: nicer error when a toplevel module has no body (#2525)letouzey
2011-04-13Extraction: opaque terms are not traversed anymore by defaultletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
2011-03-07A new command "Separate Extraction"letouzey
2010-09-24Dead code in extractionletouzey
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
2010-07-07Extraction: some more work on the (re)naming frameworkletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:02:20 +0000