aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-08-19Merge PR #12856: Adding a mention of the JSON extraction in the documentation.coqbot
Reviewed-by: jfehrle
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-08-17Merge PR #12841: Recommend replace as a replacement to cutrewrite.coqbot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-08-17Merge PR #12802: Document semantic restriction on patterns in Gallina match ↵coqbot
construct Reviewed-by: Zimmi48 Ack-by: gares Ack-by: jfehrle
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
As suggested by Laurent Thery to Chris Dams on Coq-Club. (And fix the documented syntax in the manual.)
2020-08-15Document semantic restriction on patternsJim Fehrle
2020-08-13Merge PR #12799: [stdlib] [List] Additional statements about List.repeatAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12716: deprecate prod_curry and prod_uncurryAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
Reviewed-by: erikmd Reviewed-by: herbelin
2020-08-13Merge PR #12479: Bring Int63 notations into line with stdlibAnton Trunov
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-12Additional statements about List.repeatOlivier Laurent
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
2020-08-11add deprecation to changelogYishuai Li
2020-08-11Merge PR #12717: More documentation on grammars and parsingPierre-Marie Pédrot
Reviewed-by: Zimmi48 Ack-by: herbelin Reviewed-by: ppedrot
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-09Bring Int63 notations into line with stdlibJason Gross
We also put them in a module, so users can `Require Int63. Import Int63.Int63Notations` without needing to unqualify the primitives. In particular, we change - `a \% m` into `a mod m` to correspond with the notation in ZArith - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere - `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation The old notations are still accessible as deprecated notations. Fixes #12454
2020-08-09Bring Float notations in line with stdlibJason Gross
This is a companion to #12479 as per https://github.com/coq/coq/pull/12479#issuecomment-641336039 that changes some of the PrimFloat notations: - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere We also put them in a module, so users can `Require PrimFloat. Import PrimFloat.PrimFloatNotations` without needing to unqualify the primitives. Fixes the part of #12454 about floats
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM ↵coqbot
environment variable Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-08-06Merge PR #12782: Trying to rephrase complex sentences to make them easier to ↵coqbot
read. Reviewed-by: jfehrle Ack-by: Mbodin Ack-by: corwin-of-amber
2020-08-06Trying to rephrase complex sentences to make them easier to read.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-08-03Merge PR #12772: coqdoc: Fix the “details” environmentLi-yao Xia
Reviewed-by: Lysxia
2020-07-29coqdoc: Fix the “details” environmentThomas Letan
The change introduced by 41a1d66 has broken the feature prior to its initial release. We attempt to fix the issue, and add a comment to warn feature developers in order to avoid facing the same issue again.
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
The tactics do in SSReflect uses `? @mult` rather than `? @num`.
2020-07-28Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc indexLi-yao Xia
Reviewed-by: Lysxia
2020-07-24Adding change log for #12754.Hugo Herbelin
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Fix hanging file extension.Emilio Jesus Gallego Arias
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12678: Tweak the warning for arbitrary term hints.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a ↵Théo Zimmermann
qualid in tactic notations Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-07-17Add a changelog.Pierre-Marie Pédrot
2020-07-17Documenting new primitive entry evaluable_ref usable for tactic notations.Hugo Herbelin
2020-07-17Merge PR #12670: Advertise switch to maintainer teams and credit maintainers.Emilio Jesus Gallego Arias
Reviewed-by: jfehrle
2020-07-17Merge PR #12683: Fixes #12682: printing bug with recursive notations for ↵Emilio Jesus Gallego Arias
n-ary applications used with applied references Reviewed-by: ejgallego
2020-07-17Add changelog.Pierre-Marie Pédrot
2020-07-17Wording improvements.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-07-16Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2020-07-13Advertise switch to maintainer teams and credit maintainers.Théo Zimmermann
2020-07-12Adding change log.Hugo Herbelin
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
As the text says later: > Hints should only be made available when the module they are defined in is imported, not just required.
2020-07-10Add changelog.Pierre-Marie Pédrot
2020-07-08Adding change log.Hugo Herbelin
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: gares
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:28:31 +0000