| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |