| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-30 | Merge PR #14005: Support OCaml primitives with an actual arity larger than 4. | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2021-03-26 | [ci] overlay file for #13958 | Enrico Tassi | |
| 2021-03-26 | [recordops] complete API rewrite; the module is now called [structures] | Enrico Tassi | |
| 2021-03-26 | Document as critical. | Guillaume Melquiond | |
| 2021-03-25 | Merge PR #13852: [vernac] Improve alpha-renaming in record projection types | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-03-24 | Merge PR #13993: iris_string_ident is no longer needed | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 2021-03-24 | CI Quickchick: don't install quickchick executable to opam | Gaëtan Gilbert | |
| 2021-03-24 | iris_string_ident is no longer needed | Ralf Jung | |
| 2021-03-23 | Fix debug printers | Gaëtan Gilbert | |
| 2021-03-14 | [ci] [gitlab] Remove ad-hoc mathcomp install macros | Emilio Jesus Gallego Arias | |
| They should not be necessary today as they date from the shareable pre-artifact epoch, an incur in an slowdown. | |||
| 2021-03-13 | Merge PR #13917: Add deriving lib to CI. | coqbot-app[bot] | |
| Reviewed-by: ejgallego Ack-by: SkySkimmer | |||
| 2021-03-11 | Add deriving lib to CI. | Arthur Azevedo de Amorim | |
| 2021-03-10 | Merge PR #13901: Fix list contributors | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-03-09 | Add overlay | Kazuhiko Sakaguchi | |
| 2021-03-09 | Replace cl_index with cl_typ in coercionops.ml | Kazuhiko Sakaguchi | |
| The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been replaced with `cl_typ` and `ClTypMap` respectively. | |||
| 2021-03-07 | Attempt to fix the bench after coq-core split | Gaëtan Gilbert | |
| 2021-03-06 | [vernac] Improve alpha-renaming in record projection types | Li-yao Xia | |
| 2021-03-05 | Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12) | Pierre-Marie Pédrot | |
| Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2021-03-05 | Update nixpkgs. | Théo Zimmermann | |
| To get the right version of git to use the list-contributors.sh script. | |||
| 2021-03-05 | Document the relation of the list-contributors.sh script to .mailmap. | Théo Zimmermann | |
| 2021-03-05 | Fix list-constributors.sh script. | Théo Zimmermann | |
| 2021-03-03 | [build] Split stdlib to it's own opam package. | Emilio Jesus Gallego Arias | |
| We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine. | |||
| 2021-02-27 | Add overlay | Pierre Roux | |
| 2021-02-26 | Expose Top_printers.econstr_display | Gaëtan Gilbert | |
| 2021-02-24 | Overlay for Set Debug | Gaëtan Gilbert | |
| 2021-02-22 | Fix the release process checklist with respect to the refman update. | Théo Zimmermann | |
| 2021-02-17 | Add an entry to file critical-bugs. | Guillaume Melquiond | |
| 2021-02-11 | Merge PR #13844: [vernac] pass the loc of the whole command to the interp ↵ | coqbot-app[bot] | |
| function Reviewed-by: ejgallego | |||
| 2021-02-11 | [ci] overlay for elpi | Enrico Tassi | |
| 2021-02-11 | Merge PR #13823: Update release process following coq/ceps#52. | coqbot-app[bot] | |
| Reviewed-by: ejgallego Ack-by: gares | |||
| 2021-02-11 | [vernac] pass the loc of the whole command to the interp function | Enrico Tassi | |
| 2021-02-11 | Merge PR #13847: [ci] elpi 1.13.0 | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-02-11 | overlay for coq-elpi | Enrico Tassi | |
| 2021-02-11 | [ci] elpi 1.13.0 | Enrico Tassi | |
| 2021-02-10 | Merge PR #13818: [bench] Re-enable coq-performance-tests | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-02-04 | Update release process following coq/ceps#52. | Théo Zimmermann | |
| 2021-02-04 | Merge PR #13528: [RM] Script to list the contributors between two git revisions | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Reviewed-by: gares | |||
| 2021-02-04 | Use release branch instead of master. | Théo Zimmermann | |
| 2021-02-03 | [bench] Re-enable coq-performance-tests | Jason Gross | |
| Partial revert of 6f4c61d152ad801bd571088ab99eb276b0085a04. coq-performance-tests was fixed in https://github.com/coq-community/coq-performance-tests/commit/ae8385b9471409387d0f47f01e38b866ba70bda1. Note that the current state is not optimal, as the bench does not test the native compiler at all (see #13807). | |||
| 2021-02-02 | Add VST to the set of default bench packages. | Pierre-Marie Pédrot | |
| 2021-02-02 | Merge PR #13805: Bench: remove broken packages | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2021-02-02 | Bench: don't uselessly rely on initialized opam | Gaëtan Gilbert | |
| AFAICT this init.sh call is useless. | |||
| 2021-01-29 | Bench: remove broken packages | Gaëtan Gilbert | |
| performance-tests and sf-plf have been failing for a long time without updates, there's no point wasting time partally building them. | |||
| 2021-01-27 | Add sysinit to load_printer lists | Gaëtan Gilbert | |
| 2021-01-27 | [sysinit] new component for system initialization | Enrico Tassi | |
| This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml | |||
| 2021-01-21 | Add missing item about PDF manual to release checklist. | Théo Zimmermann | |
| 2021-01-19 | Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵ | Pierre-Marie Pédrot | |
| pattern Reviewed-by: ppedrot | |||
| 2021-01-18 | Adding overlay for perennial. | Hugo Herbelin | |
| 2021-01-18 | Support locality attributes for Hint Rewrite (including export) | Gaëtan Gilbert | |
| We deprecate unspecified locality as was done for Hint. Close #13724 | |||
| 2021-01-13 | Merge PR #13740: [osx] macpack also coqidetop (for libgmp) | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |