aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/g_extraction.ml4
Commit message (Expand)AuthorAge
* 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
|/
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* issue deprecation warning for "Ocaml"Gravatar Paul Steckler2017-12-06
* use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
* Merge PR #905: [api] Remove type equalities from API.Gravatar Maxime Dénès2017-07-26
|\
* \ Merge PR #859: Extraction TestCompileGravatar Maxime Dénès2017-07-26
|\ \
| | * [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| |/ |/|
* | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
| * Extraction TestCompile foo : a new command for extraction + ocamlcGravatar Pierre Letouzey2017-07-05
|/
* 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
* Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
* Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
* Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
* Update headers.Gravatar Maxime Dénès2015-01-12
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Modulification of identifierGravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Updating headers.Gravatar herbelin2012-08-08
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* A new command "Separate Extraction"Gravatar letouzey2011-03-07
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extraction Implicits: can accept argument names instead of just positionsGravatar letouzey2010-06-10
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
* Extraction: an experimental command to get rid of some cst/constructor argumentsGravatar letouzey2010-04-30
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20