aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
AgeCommit message (Collapse)Author
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml).
2021-04-01[doc] [dune] Some tweaks from #13617Emilio Jesus Gallego Arias
Tweaks to docs that are independent / unrelated to that PR.
2021-03-26Document as critical.Guillaume Melquiond
2021-03-05Document the relation of the list-contributors.sh script to .mailmap.Théo Zimmermann
2021-02-22Fix the release process checklist with respect to the refman update.Théo Zimmermann
2021-02-17Add an entry to file critical-bugs.Guillaume Melquiond
2021-02-04Update release process following coq/ceps#52.Théo Zimmermann
2021-02-04Merge PR #13528: [RM] Script to list the contributors between two git revisionscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares
2021-02-04Use release branch instead of master.Théo Zimmermann
2021-01-21Add missing item about PDF manual to release checklist.Théo Zimmermann
2021-01-04Document the change of case representation.Pierre-Marie Pédrot
2020-12-15Merge PR #13615: Document the manual tasks that I need to do at each release.coqbot-app[bot]
Reviewed-by: ejgallego
2020-12-11Removing non relevant argument binding_kind of GLocalDef.Hugo Herbelin
2020-12-11Document the manual tasks that I need to do at each release.Théo Zimmermann
2020-12-09[rm] announcements to discourseEnrico Tassi
2020-12-08Update dev/doc/release-process.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-07[rm] manual is uploaded by CIEnrico Tassi
2020-12-07[rm] update instructions for windows signingEnrico Tassi
2020-12-04[rm] clarify process for is_a_released_version = trueEnrico Tassi
2020-12-04[rm] update git commands to push tagsEnrico Tassi
2020-11-30list-contributors scriptMatthieu Sozeau
2020-11-27[RM] script to notify "platform" projects to tagEnrico Tassi
2020-11-20Make 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-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-02Update screenshot of shield icon (shown in CONTRIBUTING).Théo Zimmermann
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-14Deprecating 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-10Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵Hugo Herbelin
deprecated.
2020-10-08Dropping 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-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-28Document the ocamlformat changes.Pierre-Marie Pédrot
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-09Update dev/doc/critical-bugsPierre Roux
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-15Update dev/doc/release-process.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-05-15Clarify release-process.mdEnrico Tassi
2020-05-10Merge PR #12286: [sphinx] Add links to other versions of the refmanThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-09[sphinx] Add links to other versions of the refmanClément Pit-Claudel
2020-04-26Document 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-22Centralizing 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:30:48 +0000