aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop_bin.ml
Commit message (Collapse)AuthorAge
* [make] remove unneeded generated file "tolink.ml"Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364.
* [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.