aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
Commit message (Collapse)AuthorAge
* 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).
| * Move dev/doc/changes to Markdown.Gravatar Théo Zimmermann2017-08-29
|/ | | | | And remove old French part. And move part about the plugin API to the right section.
* Merge PR #819: Cleanup old thingsGravatar Maxime Dénès2017-08-29
|\
* | Mention tclINDEPENDENTL (#349) in dev/doc/changes.Gravatar Théo Zimmermann2017-08-16
| |
| * Remove obsolete filesGravatar Gaëtan Gilbert2017-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-conversionGravatar Gaëtan Gilbert2017-08-01
|/ | | | This gives syntax highlighting in Coq-aware editors.
* Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
* \ \ Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceGravatar Maxime Dénès2017-07-28
|\ \ \
| | | * [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |_|/ |/| | | | | | | | Minor clean up, no sense in having these as they do nothing.
| | * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | |
* | | Merge PR #886: Fixing what was presumably a typo in the naming conventions fileGravatar Maxime Dénès2017-07-26
|\ \ \ | |_|/ |/| |
* | | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
| | |
| * | Fixing what was presumably a typo in the naming conventions file.Gravatar Hugo Herbelin2017-07-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed, "forall x, op x x = x" in not in the list, while this is one of the two standard meanings of idempotence. So, knowing that x, y, ... and not n are used elsewhere for variables names, and elt for constants. Moreover, it is probable that before using consistently x, y and z, I had also used m and n, sometimes. So, a convergent probability that it is (just) a typo.
* | | Fix a typo in dev/changes.Gravatar Pierre-Marie Pédrot2017-07-14
| | |
* | | Document the changes in API brought by this series of patches.Gravatar Pierre-Marie Pédrot2017-07-14
|/ /
| * Makefile: fails if some .vo or .cm* file has no sourceGravatar Pierre Letouzey2017-07-05
|/ | | | | | | | | | | This should help preventing weird compilation failures due to leftover object files after deleting or moving some source files By the way: - use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason for the suggestion) - rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more than version control stuff nowadays
* [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
* Merge PR#749: Normalize deprecation notices of ./configureGravatar Maxime Dénès2017-06-14
|\
* \ Merge PR#622: Change the default flag value for Refine.refineGravatar Maxime Dénès2017-06-14
|\ \
| * | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| | |
| * | Documenting the change of default flag value of Refine.refine.Gravatar Pierre-Marie Pédrot2017-06-13
| | |
| | * Normalize deprecation notices of ./configureGravatar Théo Zimmermann2017-06-11
| |/ | | | | | | Always output a warning on stderr when a deprecated option is used.
* / Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
|/ | | | | | | | | | | | | | This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
* Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\
* | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
| * Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
|/ | | | | | Constrintern.pf_global returns a global_reference, not a constr, adapt plugins accordingly, properly registering universes where necessary.
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 08:59:18 +0000