aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/table.ml
Commit message (Expand)AuthorAge
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Gravatar Maxime Dénès2018-03-08
|\
| * An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Extraction : minor support stuff for the new Extraction Compute pluginGravatar Pierre Letouzey2017-10-04
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
| * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 16:21:00 +0000