aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/table.ml
Commit message (Expand)AuthorAge
* [safe-string] plugins/extractionGravatar Emilio Jesus Gallego Arias2017-03-14
* Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
* Extraction: avoid deprecated functions of module StringGravatar Pierre Letouzey2017-02-07
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
|/
* Extraction: more cautious use of intermediate result caching (fix #3923)Gravatar Pierre Letouzey2015-12-15
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
* Update headers.Gravatar Maxime Dénès2015-01-12
* Extraction: minor tweaks to ease ongoing experiments about LambdaGravatar Pierre Letouzey2015-01-11
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* bwaa, a Pervasive.compareGravatar pboutill2013-05-30
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Extraction AccessOpaque is now activated again by default (#2952)Gravatar letouzey2013-03-18
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Classops : avoid some use of GmapGravatar letouzey2013-02-19
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Added a CString module.Gravatar ppedrot2012-11-13
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Experimental support for a comment in the files' preamble in extraction.Gravatar aspiwack2012-08-24
* Add option Set/Unset Extraction Conservative Types.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* Dump referencesGravatar pboutill2012-08-05
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Extraction: Richer patterns in matchs as proposed by P.N. TollitteGravatar letouzey2011-11-28