aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
AgeCommit message (Collapse)Author
2018-02-22Tweak developer documentation.Jim Fehrle
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
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.
2018-02-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
longer use camlp4.
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
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.
2018-02-05[stm] [toplevel] Make loadpath a parameter of the document.Emilio Jesus Gallego Arias
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...
2018-01-23Merge PR #6629: Archive COMPATIBILITYMaxime Dénès
2018-01-22Archive COMPATIBILITY.Théo Zimmermann
2018-01-22Merge PR #6550: Remove outdated note about rlwrap in setup.txtMaxime Dénès
2018-01-08Stop talking about debian in "A note about rlwrap"Gaëtan Gilbert
Debian stable version is 0.42-3 right now.
2018-01-08Merge PR #6501: Document use of ocamldebug from the command line in ↵Maxime Dénès
Cygwin/Windows
2017-12-29Add instructions for debugging from the command line (and in Windows)Jim Fehrle
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
2017-12-27[API] remove large file containing duplicate interfacesEnrico Tassi
... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
2017-12-26[ide] [doc] Document tweak to Query call.Emilio Jesus Gallego Arias
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-10[build] Remove coqmktop in favor of ocamlfind.Emilio Jesus Gallego Arias
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.
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
2017-11-29[lib] [api] Introduce record for `object_prefix`Emilio Jesus Gallego Arias
This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
2017-11-13Change OCAMLRUNPARAM warning to mention OCaml 4.06Paul Steckler
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-03Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵Maxime Dénès
dev/doc/changes.
2017-11-03Merge PR #6024: Update of Coq version historyMaxime Dénès
2017-11-02Using a specific function to register vernac printers.Hugo Herbelin
2017-10-27Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.Théo Zimmermann
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
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.
2017-10-26Updating version history wrt 8.7.Hugo Herbelin
2017-10-26Updating version history wrt 8.6.Hugo Herbelin
2017-10-26Updating version history wrt 8.5.Hugo Herbelin
2017-10-10[configure] Support for flambda flags.Emilio Jesus Gallego Arias
We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
2017-10-06Extract changes to the XML protocol from its docThéo Zimmermann
2017-10-06Make the XML protocol doc more version-independentThéo Zimmermann
2017-09-19Improve documentation of Status message.Maxime Dénès
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Maxime Dénès
top of the linking chain.
2017-09-15Merge PR #962: Move dev/doc/changes to Markdown.Maxime Dénès
2017-08-31Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaroundMaxime Dénès
2017-08-29mention issue with OCAMLRUNPARAM and ocamldebugPaul Steckler
2017-08-29[general] Merge parsing with highparsing, put toplevel at the top of the ↵Emilio Jesus Gallego Arias
linking chain.
2017-08-29Adapt debugging doc to configure/Makefile changes.Théo Zimmermann
2017-08-29Move debugging to Markdown.Théo Zimmermann
With a minimal diff (so I'm not putting quotes ` ` around all the code).
2017-08-29Move dev/doc/changes to Markdown.Théo Zimmermann
And remove old French part. And move part about the plugin API to the right section.
2017-08-29Merge PR #819: Cleanup old thingsMaxime Dénès
2017-08-16Mention tclINDEPENDENTL (#349) in dev/doc/changes.Théo Zimmermann
2017-08-01Remove obsolete filesGaëtan Gilbert
db_printers just isn't used. api.txt is superseded by the API OCaml interface.
2017-08-01Add .v extension to dev/doc/notes-on-conversionGaëtan Gilbert
This gives syntax highlighting in Coq-aware editors.
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:44:46 +0000