Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | [stm] [toplevel] Make loadpath a parameter of the document. | 2018-02-05 | |
| | | | | | | | | | | | | | | We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc... | ||
* | Merge PR #6629: Archive COMPATIBILITY | 2018-01-23 | |
|\ | |||
| * | Archive COMPATIBILITY. | 2018-01-22 | |
| | | |||
* | | Merge PR #6550: Remove outdated note about rlwrap in setup.txt | 2018-01-22 | |
|\ \ | |/ |/| | |||
| * | Stop talking about debian in "A note about rlwrap" | 2018-01-08 | |
| | | | | | | | | Debian stable version is 0.42-3 right now. | ||
* | | Merge PR #6501: Document use of ocamldebug from the command line in ↵ | 2018-01-08 | |
|\ \ | |/ |/| | | | Cygwin/Windows | ||
| * | Add instructions for debugging from the command line (and in Windows) | 2017-12-29 | |
| | | | | | | | | Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows) | ||
* | | [API] remove large file containing duplicate interfaces | 2017-12-27 | |
| | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | ||
* | | [ide] [doc] Document tweak to Query call. | 2017-12-26 | |
|/ | |||
* | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | 2017-12-18 | |
|\ | |||
| * | [econstr] Switch constrintern API to non-imperative style. | 2017-12-15 | |
| | | | | | | | | | | We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there. | ||
* | | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | 2017-12-14 | |
|\ \ | |/ |/| | |||
| * | [build] Remove coqmktop in favor of ocamlfind. | 2017-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. | ||
* | | [api] Remove yet another type alias. | 2017-12-09 | |
| | | |||
| * | [lib] Rename Profile to CProfile | 2017-12-09 | |
|/ | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`. | ||
* | [lib] [api] Introduce record for `object_prefix` | 2017-11-29 | |
| | | | | | This is a minor cleanup adding a record in a try to structure the state living in `Lib`. | ||
* | Change OCAMLRUNPARAM warning to mention OCaml 4.06 | 2017-11-13 | |
| | |||
* | [api] Remove 8.7 ML-deprecated functions. | 2017-11-07 | |
| | |||
* | Merge PR #6047: A generic printer for ltac values | 2017-11-03 | |
|\ | |||
* \ | Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵ | 2017-11-03 | |
|\ \ | | | | | | | | | | dev/doc/changes. | ||
* \ \ | Merge PR #6024: Update of Coq version history | 2017-11-03 | |
|\ \ \ | |||
| | | * | Using a specific function to register vernac printers. | 2017-11-02 | |
| |_|/ |/| | | |||
| | * | Mention the migration from Bugzilla to GitHub issues in dev/doc/changes. | 2017-10-27 | |
| | | | |||
* | | | Passing around the flag for injection so that tactics calling inj at | 2017-10-26 | |
| |/ |/| | | | | | | | | | | | | | | | | | ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281. | ||
| * | Updating version history wrt 8.7. | 2017-10-26 | |
| | | |||
| * | Updating version history wrt 8.6. | 2017-10-26 | |
| | | |||
| * | Updating version history wrt 8.5. | 2017-10-26 | |
|/ | |||
* | [configure] Support for flambda flags. | 2017-10-10 | |
| | | | | | | | | | We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ``` | ||
* | Extract changes to the XML protocol from its doc | 2017-10-06 | |
| | |||
* | Make the XML protocol doc more version-independent | 2017-10-06 | |
| | |||
* | Improve documentation of Status message. | 2017-09-19 | |
| | |||
* | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵ | 2017-09-15 | |
|\ | | | | | | | top of the linking chain. | ||
* \ | Merge PR #962: Move dev/doc/changes to Markdown. | 2017-09-15 | |
|\ \ | |||
* \ \ | Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaround | 2017-08-31 | |
|\ \ \ | |||
| * | | | mention issue with OCAMLRUNPARAM and ocamldebug | 2017-08-29 | |
| | | | | |||
| | | * | [general] Merge parsing with highparsing, put toplevel at the top of the ↵ | 2017-08-29 | |
| | |/ | |/| | | | | | | | linking chain. | ||
* | | | Adapt debugging doc to configure/Makefile changes. | 2017-08-29 | |
| | | | |||
* | | | Move debugging to Markdown. | 2017-08-29 | |
|/ / | | | | | With a minimal diff (so I'm not putting quotes ` ` around all the code). | ||
| * | Move dev/doc/changes to Markdown. | 2017-08-29 | |
|/ | | | | | And remove old French part. And move part about the plugin API to the right section. | ||
* | Merge PR #819: Cleanup old things | 2017-08-29 | |
|\ | |||
* | | Mention tclINDEPENDENTL (#349) in dev/doc/changes. | 2017-08-16 | |
| | | |||
| * | Remove obsolete files | 2017-08-01 | |
| | | | | | | | | | | db_printers just isn't used. api.txt is superseded by the API OCaml interface. | ||
| * | Add .v extension to dev/doc/notes-on-conversion | 2017-08-01 | |
|/ | | | | This gives syntax highlighting in Coq-aware editors. | ||
* | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | 2017-08-01 | |
|\ | |||
* \ | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | 2017-07-31 | |
|\ \ | |||
* \ \ | Merge PR #852: Makefile: fails if some .vo or .cm* file has no source | 2017-07-28 | |
|\ \ \ | |||
| | | * | [toplevel] Remove long ago deprecated and NOOP options. | 2017-07-27 | |
| |_|/ |/| | | | | | | | | Minor clean up, no sense in having these as they do nothing. | ||
| | * | deprecate Pp.std_ppcmds type alias | 2017-07-27 | |
| | | | |||
* | | | Merge PR #886: Fixing what was presumably a typo in the naming conventions file | 2017-07-26 | |
|\ \ \ | |_|/ |/| | | |||
* | | | [API] Remove `open API` in ml files in favor of `-open API` flag. | 2017-07-17 | |
| | | |