aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
filtered-only show Ltac2 tags outside of ltac2.rst
2020-07-08Make local nonterminal definitions unique when necessaryJim Fehrle
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
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵Gaëtan Gilbert
patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2020-07-01Add a changelog.Pierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-29Merge PR #12372: [declare] Refactor constant information into a record.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-27Merge PR #12583: [test-suite] Fix dependencies of modules/ filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-26Mention VSCoq with respect to _CoqProjectCarl Patenaude-Poulin
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
We unify information about constants so it is shared among all the paths [interactive, NI, obligations]. IMHO the current setup looks pretty good, with information split into a per-constant record `CInfo.t` and variables affecting mutual definitions at once, which live in `Info.t`. Main information outside our `Info` record is `opaque`, which is provided at different moments in several cases. There are a few nits regarding interactive proofs, which will go away in the next commits.
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
This is in preparation for the next commit which will clean-up the current API flow in `Declare`.
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
This improves the interface, and allows even more sealing of the API. This is yet work in progress.
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface.
2020-06-26Credit Erik Martin-Dorel for work on Docker.Théo Zimmermann
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
Fixes #12582 The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime `plik.v.log` is older than `Nat.vo`. This is circular, and results in `make` considering all of the `modules/` tests out-of-date on any fresh run.
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
Fixes #12571.
2020-06-23Merge PR #12562: CoqIDE: accept to open files with invalid namesMichael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: SkySkimmer
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
Reviewed-by: fajb
2020-06-22CoqIDE: accept to open files with invalid namesVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 07:09:23 +0000