| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-13 | Change OCAMLRUNPARAM warning to mention OCaml 4.06 | Paul Steckler | |
| 2017-11-07 | [api] Remove 8.7 ML-deprecated functions. | Emilio Jesus Gallego Arias | |
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-03 | Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵ | Maxime Dénès | |
| dev/doc/changes. | |||
| 2017-11-03 | Merge PR #6024: Update of Coq version history | Maxime Dénès | |
| 2017-11-02 | Using a specific function to register vernac printers. | Hugo Herbelin | |
| 2017-10-27 | Mention the migration from Bugzilla to GitHub issues in dev/doc/changes. | Théo Zimmermann | |
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo 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-26 | Updating version history wrt 8.7. | Hugo Herbelin | |
| 2017-10-26 | Updating version history wrt 8.6. | Hugo Herbelin | |
| 2017-10-26 | Updating 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-06 | Extract changes to the XML protocol from its doc | Théo Zimmermann | |
| 2017-10-06 | Make the XML protocol doc more version-independent | Théo Zimmermann | |
| 2017-09-19 | Improve documentation of Status message. | Maxime Dénès | |
| 2017-09-15 | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵ | Maxime Dénès | |
| top of the linking chain. | |||
| 2017-09-15 | Merge PR #962: Move dev/doc/changes to Markdown. | Maxime Dénès | |
| 2017-08-31 | Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaround | Maxime Dénès | |
| 2017-08-29 | mention issue with OCAMLRUNPARAM and ocamldebug | Paul Steckler | |
| 2017-08-29 | [general] Merge parsing with highparsing, put toplevel at the top of the ↵ | Emilio Jesus Gallego Arias | |
| linking chain. | |||
| 2017-08-29 | Adapt debugging doc to configure/Makefile changes. | Théo Zimmermann | |
| 2017-08-29 | Move debugging to Markdown. | Théo Zimmermann | |
| With a minimal diff (so I'm not putting quotes ` ` around all the code). | |||
| 2017-08-29 | Move 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-29 | Merge PR #819: Cleanup old things | Maxime Dénès | |
| 2017-08-16 | Mention tclINDEPENDENTL (#349) in dev/doc/changes. | Théo Zimmermann | |
| 2017-08-01 | Remove obsolete files | Gaëtan Gilbert | |
| db_printers just isn't used. api.txt is superseded by the API OCaml interface. | |||
| 2017-08-01 | Add .v extension to dev/doc/notes-on-conversion | Gaëtan Gilbert | |
| This gives syntax highlighting in Coq-aware editors. | |||
| 2017-08-01 | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | Maxime Dénès | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-28 | Merge PR #852: Makefile: fails if some .vo or .cm* file has no source | Maxime Dénès | |
| 2017-07-27 | [toplevel] Remove long ago deprecated and NOOP options. | Emilio Jesus Gallego Arias | |
| Minor clean up, no sense in having these as they do nothing. | |||
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Merge PR #886: Fixing what was presumably a typo in the naming conventions file | Maxime Dénès | |
| 2017-07-17 | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | |
| 2017-07-16 | Fixing what was presumably a typo in the naming conventions file. | Hugo Herbelin | |
| 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. | |||
| 2017-07-14 | Fix a typo in dev/changes. | Pierre-Marie Pédrot | |
| 2017-07-14 | Document the changes in API brought by this series of patches. | Pierre-Marie Pédrot | |
| 2017-07-05 | Makefile: fails if some .vo or .cm* file has no source | Pierre Letouzey | |
| 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 | |||
| 2017-06-18 | [ide] Add route_id parameter to query call. | Emilio Jesus Gallego Arias | |
| 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 ####. | |||
| 2017-06-14 | Merge PR#749: Normalize deprecation notices of ./configure | Maxime Dénès | |
| 2017-06-14 | Merge PR#622: Change the default flag value for Refine.refine | Maxime Dénès | |
| 2017-06-13 | Dualize the unsafe flag of refine into typecheck and make it mandatory. | Pierre-Marie Pédrot | |
| 2017-06-13 | Documenting the change of default flag value of Refine.refine. | Pierre-Marie Pédrot | |
| 2017-06-11 | Normalize deprecation notices of ./configure | Théo Zimmermann | |
| Always output a warning on stderr when a deprecated option is used. | |||
| 2017-06-04 | Added support for a side effect on constants in reduction functions. | Thomas Sibut-Pinote | |
| 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. | |||
| 2017-06-01 | Merge PR#696: Trunk+cleanup constr of global | Maxime Dénès | |
| 2017-05-31 | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin | |
| 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. | |||
| 2017-05-29 | Cleanup: removal of constr_of_global. | Matthieu Sozeau | |
| Constrintern.pf_global returns a global_reference, not a constr, adapt plugins accordingly, properly registering universes where necessary. | |||
| 2017-05-29 | Merge PR#512: [cleanup] Unify all calls to the error function. | Maxime Dénès | |
| 2017-05-27 | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |