| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update headers following #6543. |  Théo Zimmermann | 2018-02-27 |
| | | |||
| * | Change references to CAMLP4 to CAMLP5 to be more accurate since we no |  Jim Fehrle | 2018-02-17 |
| | | | | | longer use camlp4. | ||
| * | [API] Remove `open API` in ml files in favor of `-open API` flag. |  Emilio Jesus Gallego Arias | 2017-07-17 |
| | | |||
| * | Bump year in headers. |  Pierre-Marie Pédrot | 2017-07-04 |
| | | |||
| * | Put all plugins behind an "API". |  Matej Kosik | 2017-06-07 |
| | | |||
| * | Merging Stdarg and Constrarg. | Pierre-Marie Pédrot | 2016-09-21 |
| | | | | | | | There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore. | ||
| * | Compilation via pack for plugins of the stdlib |  Pierre Letouzey | 2016-06-08 |
| | | | | | | | | | | | | | | | | | | | | | | | | | For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts. | ||
| * | Removing dead code and unused opens. | Pierre-Marie Pédrot | 2016-05-08 |
| | | |||
| * | Removing the special status of generic entries defined by Coq itself. | Pierre-Marie Pédrot | 2016-03-17 |
| | | | | | | | | | | | | The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. | ||
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| | | |||
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| | | |||
| * | Avoiding introducing yet another convention in naming files. |  Hugo Herbelin | 2015-01-08 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |