aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
Commit message (Collapse)AuthorAge
* Some advice about merge script dependencies.Gravatar Théo Zimmermann2018-04-05
| | | | Including: how to create a GPG key.
* Improve the MERGING doc.Gravatar Théo Zimmermann2018-04-05
| | | | In particular, describes what to do with overlays.
* More precise wording about the merge process.Gravatar Maxime Dénès2018-03-23
| | | | | In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases.
* Refine a bit the decentralized merging process.Gravatar Maxime Dénès2018-03-21
| | | | | | | | | | | | We make GitHub assign only principal maintainers as reviewers. This reduces the level of noise (PRs with 10 code owners), and makes it easy for the assignee to check if all reviews have been completed (all reviewers in the list have to approve the PR, which was not the case before if two reviewers were assigned for the same component). This change means that when a principal maintainer submits a patch touching the component they own, they should ask a review from the secondary maintainer.
* Describe new merging process.Gravatar Maxime Dénès2018-03-19
|
* document -profile in dev/doc/setup.txtGravatar Enrico Tassi2018-03-06
|
* Merge PR #6812: Rename release_lexer_state to the more descriptive ↵Gravatar Maxime Dénès2018-02-28
|\ | | | | | | get_lexer_state.
| * Tweak developer documentation.Gravatar Jim Fehrle2018-02-22
| |
* | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
|/ | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\
* | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | longer use camlp4.
| * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
|/ | | | | | | | | | | | | | In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
* [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-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 COMPATIBILITYGravatar Maxime Dénès2018-01-23
|\
| * Archive COMPATIBILITY.Gravatar Théo Zimmermann2018-01-22
| |
* | Merge PR #6550: Remove outdated note about rlwrap in setup.txtGravatar Maxime Dénès2018-01-22
|\ \ | |/ |/|
| * Stop talking about debian in "A note about rlwrap"Gravatar Gaëtan Gilbert2018-01-08
| | | | | | | | Debian stable version is 0.42-3 right now.
* | Merge PR #6501: Document use of ocamldebug from the command line in ↵Gravatar Maxime Dénès2018-01-08
|\ \ | |/ |/| | | Cygwin/Windows
| * Add instructions for debugging from the command line (and in Windows)Gravatar Jim Fehrle2017-12-29
| | | | | | | | Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
* | [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-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.Gravatar Emilio Jesus Gallego Arias2017-12-26
|/
* Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\
| * [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-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.Gravatar Maxime Dénès2017-12-14
|\ \ | |/ |/|
| * [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.
* | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |
| * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-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`Gravatar Emilio Jesus Gallego Arias2017-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.06Gravatar Paul Steckler2017-11-13
|
* [api] Remove 8.7 ML-deprecated functions.Gravatar Emilio Jesus Gallego Arias2017-11-07
|
* Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\
* \ Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵Gravatar Maxime Dénès2017-11-03
|\ \ | | | | | | | | | dev/doc/changes.
* \ \ Merge PR #6024: Update of Coq version historyGravatar Maxime Dénès2017-11-03
|\ \ \
| | | * Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
| |_|/ |/| |
| | * Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.Gravatar Théo Zimmermann2017-10-27
| | |
* | | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-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.Gravatar Hugo Herbelin2017-10-26
| |
| * Updating version history wrt 8.6.Gravatar Hugo Herbelin2017-10-26
| |
| * Updating version history wrt 8.5.Gravatar Hugo Herbelin2017-10-26
|/
* [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-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 docGravatar Théo Zimmermann2017-10-06
|
* Make the XML protocol doc more version-independentGravatar Théo Zimmermann2017-10-06
|
* Improve documentation of Status message.Gravatar Maxime Dénès2017-09-19
|
* Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Gravatar Maxime Dénès2017-09-15
|\ | | | | | | top of the linking chain.
* \ Merge PR #962: Move dev/doc/changes to Markdown.Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaroundGravatar Maxime Dénès2017-08-31
|\ \ \
| * | | mention issue with OCAMLRUNPARAM and ocamldebugGravatar Paul Steckler2017-08-29
| | | |
| | | * [general] Merge parsing with highparsing, put toplevel at the top of the ↵Gravatar Emilio Jesus Gallego Arias2017-08-29
| | |/ | |/| | | | | | | linking chain.
* | | Adapt debugging doc to configure/Makefile changes.Gravatar Théo Zimmermann2017-08-29
| | |
* | | Move debugging to Markdown.Gravatar Théo Zimmermann2017-08-29
|/ / | | | | With a minimal diff (so I'm not putting quotes ` ` around all the code).