aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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-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
2020-06-21Add index for coqdoc.Théo Zimmermann
Fixes #12545.
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
Hope this is enough, also looking at https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-06-11Merge PR #12481: Minor improvements to the sections on basics and sorts.Emilio Jesus Gallego Arias
Reviewed-by: jfehrle
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
Ack-by: Zimmi48 Reviewed-by: erikmd Reviewed-by: silene
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n ↵Vincent Semeria
to 1/2^n Reviewed-by: VincentSe
2020-06-09Merge sections on functions and function types.Théo Zimmermann
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
2020-06-09Minor improvements to the section on basics.Théo Zimmermann
2020-06-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-09Summary of changes for 8.12Matthieu Sozeau
Includes fixes to changes by Jim, Enrico and Théo Fix local links, for 8.12 and 8.11
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
- by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except - don't generate a name for cmdv and tacv - generate more flexibily for exn, warn and attr
2020-06-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
(Sphinx notations don't support these.)
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-06-08Refactor SELF code for clarityJim Fehrle
Handle SELF within nested constructs more clearly
2020-06-08Fix 12483Pierre Roux
2020-06-07[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_linesClément Pit-Claudel
2020-06-07Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: ↵Clément Pit-Claudel
directive
2020-06-06Match only a single line as the coqtop promptJim Fehrle
(the previous expression was including some expected output)
2020-06-06Merge PR #12380: Fix #12361 (indexing issues in the PDF)Théo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:54:22 +0000