| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-01-21 | Add missing item about PDF manual to release checklist. | Théo Zimmermann | |
| 2021-01-04 | Document the change of case representation. | Pierre-Marie Pédrot | |
| 2020-12-15 | Merge PR #13615: Document the manual tasks that I need to do at each release. | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 2020-12-11 | Removing non relevant argument binding_kind of GLocalDef. | Hugo Herbelin | |
| 2020-12-11 | Document the manual tasks that I need to do at each release. | Théo Zimmermann | |
| 2020-12-09 | [rm] announcements to discourse | Enrico Tassi | |
| 2020-12-08 | Update dev/doc/release-process.md | Enrico Tassi | |
| Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> | |||
| 2020-12-07 | [rm] manual is uploaded by CI | Enrico Tassi | |
| 2020-12-07 | [rm] update instructions for windows signing | Enrico Tassi | |
| 2020-12-04 | [rm] clarify process for is_a_released_version = true | Enrico Tassi | |
| 2020-12-04 | [rm] update git commands to push tags | Enrico Tassi | |
| 2020-11-30 | list-contributors script | Matthieu Sozeau | |
| 2020-11-27 | [RM] script to notify "platform" projects to tag | Enrico Tassi | |
| 2020-11-20 | Make sure accumulators do not exceed the minor heap (partly fix #11170). | Guillaume Melquiond | |
| Accumulators can grow arbitrarily large, even when well-typed. So, this commit makes sure they are allocated on the major heap when they are too large. If so, fields need to be filled with caml_initialize, in case they point to the minor heap. | |||
| 2020-11-15 | [dune] [opam] Generate opam files automatically using Dune. | Emilio Jesus Gallego Arias | |
| - closes #12376 : dune version is now consistent as suggested - cc #12858 : coqide and coqide-server do no depend on ocamlfind when built this way. - closes #13372 : more precision in the license identifier | |||
| 2020-11-12 | Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and pop | coqbot-app[bot] | |
| Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego | |||
| 2020-11-12 | Change Dumpglob.pause and Dumpglob.continue into push and pop | Lasse Blaauwbroek | |
| Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-11-12 | Add documentation about the soundness bug. | Pierre-Marie Pédrot | |
| 2020-11-02 | Update screenshot of shield icon (shown in CONTRIBUTING). | Théo Zimmermann | |
| 2020-10-27 | Rename tactic_expr -> ltac_expr | Jim Fehrle | |
| 2020-10-14 | Deprecating wit_var to the benefit of its synonymous wit_hyp. | Hugo Herbelin | |
| Note: "hyp" was documented in Ltac Notation chapter but "var" was not. | |||
| 2020-10-10 | Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵ | Hugo Herbelin | |
| deprecated. | |||
| 2020-10-08 | Dropping the misleading int argument of Pp.h. | Hugo Herbelin | |
| An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended. | |||
| 2020-10-04 | Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵ | coqbot-app[bot] | |
| -> "constr" Reviewed-by: herbelin Ack-by: Zimmi48 | |||
| 2020-10-04 | Remove prefixes on nonterminal names, e.g. "constr:" and "Prim." | Jim Fehrle | |
| 2020-09-28 | Document the ocamlformat changes. | Pierre-Marie Pédrot | |
| 2020-09-22 | Fixes #9716, #13004: don't drop the qualifier of quotations at printing time. | Hugo Herbelin | |
| 2020-08-03 | More documentation on grammars and parsing | Jim Fehrle | |
| 2020-07-01 | UIP in SProp | Gaëtan Gilbert | |
| 2020-06-09 | Update dev/doc/critical-bugs | Pierre Roux | |
| 2020-05-18 | Update release-process.md | Enrico Tassi | |
| 2020-05-18 | Update release-process.md | Enrico Tassi | |
| 2020-05-18 | Update to 8.13. | Théo Zimmermann | |
| Part of this PR was automatically generated by running dev/doc/update-compat.py --master | |||
| 2020-05-15 | Update dev/doc/release-process.md | Enrico Tassi | |
| Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> | |||
| 2020-05-15 | Clarify release-process.md | Enrico Tassi | |
| 2020-05-10 | Merge PR #12286: [sphinx] Add links to other versions of the refman | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2020-05-09 | [sphinx] Add links to other versions of the refman | Clément Pit-Claudel | |
| 2020-04-26 | Document the signing procedure of released binary packages. | Pierre-Marie Pédrot | |
| 2020-04-15 | [dev] [doc] Changes. | Emilio Jesus Gallego Arias | |
| 2020-04-11 | [dune] [stdlib] Build the standard library natively with Dune. | Emilio Jesus Gallego Arias | |
| This completes a pure Dune bootstrap of Coq. There is still the question if we should modify `coqdep` so it does output a dependency on `Init.Prelude.vo` in certain cases. TODO: We still double-add `theories` and `plugins` [in coqinit and in Dune], this should be easy to clean up. Setting `libs_init_load_path` does give a correct build indeed; however we still must call this for compatibility? | |||
| 2020-03-22 | Centralizing all kinds of numeral string management in numTok.ml. | Hugo Herbelin | |
| Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him. | |||
| 2020-03-19 | [ocamformat] Update to 0.13.0 | Emilio Jesus Gallego Arias | |
| We include the `version=0.13.0` field that should help users not to use the wrong version. `disable=true` still seems a noop with `dune`. There are some minor changes in the way comments are formatted; I'm unsure if this is due to the `wrap-comments` option; as always; tweaks to the config are most welcome. | |||
| 2020-03-13 | Deprecation of catchable_exception, to be replaced by noncritical in try-with. | Hugo Herbelin | |
| 2020-03-06 | Merge PR #11717: [dune] [ocamldebug] Improve ocamldebug rules | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2020-03-01 | [dune] [doc] Be more explicit coqtop dependencies | Emilio Jesus Gallego Arias | |
| Fixes #11726 | |||
| 2020-02-29 | [dune] [ocamldebug] Improve ocamldebug rules | Emilio Jesus Gallego Arias | |
| We provide the closure of the dependencies manually. This is still a hack, but not so bad given that the `source`'d files still do contain that duplication too. Dune should provide this functionality so we can replace both this rule and the source files. Actually, that's not hard to implement, `utop` already supports a printer attribute so these are loaded automatically, so the ocamldebug mode could do the same. Should fix #11716 | |||
| 2020-02-24 | [exn] Forbid raising in exn printers, make them return Pp.t option | Emilio Jesus Gallego Arias | |
| Raising inside exception printers is quite tricky as the order of registration for printers will indeed depend on the linking order. We thus forbid this, and make our API closer to the upstream `Printexn` by having printers return an option type. | |||
| 2020-02-22 | Making structure of type "tolerability" and related clearer. | Hugo Herbelin | |
| Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |