aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-05-09[sphinx] Add links to other versions of the refmanClément Pit-Claudel
2020-05-08Merge PR #12272: Cleanup formatting in .. coqtop:: directivesClément Pit-Claudel
Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
Reviewed-by: pi8027 Reviewed-by: zeldovich
2020-05-08Recursively look for the first string nodeQuentin Carbonneaux
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-08Merge PR #12281: [doc] named lemmas can be Saved tooThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-08Merge PR #12268: Add an example to motivate strictly positive occurrences checkThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-08Merge PR #12068: Coqide completion: tentative fix for #11943Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`. Fixes #12257 Fixes #12258
2020-05-06Adding properties about implb.Hugo Herbelin
This addresses a question on gitter (April 4).
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
2020-05-04Merge PR #12211: When TIMED=1, emit timing info for OCaml filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-04add order properties about boolOlivier Laurent
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
2020-05-02Adding change logs for PR #12121.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Also including feedback from Enrico Tassi.
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
There was also a non truly recursive in the doc.
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-05-01Preserve vernac chapter.Théo Zimmermann
2020-05-01Extract two new files out of Gallina chapter.Théo Zimmermann
2020-05-01Create section on writing libraries with only deprecated attributes.Théo Zimmermann
2020-05-01Extract deprecated attribute from Gallina chapter.Théo Zimmermann
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Remove lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Create basics out of sections from Gallina and Vernac chapters.Théo Zimmermann
2020-05-01Create section on basics with just flags, options and tables.Théo Zimmermann
2020-05-01Extract flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Create section on basics with just lexical conventions and attributes.Théo Zimmermann
2020-05-01Extract lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat. The required declarations are now added in ZifyInst.
2020-04-29When TIMED=1, emit timing info for OCaml filesJason Gross
2020-04-29Merge PR #11606: [tools] Add memory stats to tables by defaultEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-29Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ↵Emilio Jesus Gallego Arias
in record tuples Reviewed-by: ejgallego
2020-04-29Merge PR #12150: Support in-line glossary definitions and references with an ↵Clément Pit-Claudel
index Ack-by: Zimmi48
2020-04-29Merge PR #12195: [doc] [sphinx] Run in silent mode by defaultThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29Support in-line glossary entries and referencesJim Fehrle
with an index
2020-04-28[doc] [sphinx] Be silent when running latexmkEmilio Jesus Gallego Arias
This is actually supported by Sphinx directly.
2020-04-28[doc] [sphinx] Run in silent mode by defaultEmilio Jesus Gallego Arias
The convention in the dune build is to be silent except for warnings and errors, so they don't go unnoticed. We could have this controlled by a variable if needed (likely would require some support from Dune?) Solves part of #12194
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: jfehrle
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-27Merge PR #12073: Split off Nsatz tactic part into Nsatz_tacticPierre-Marie Pédrot
Reviewed-by: anton-trunov Reviewed-by: ppedrot
2020-04-27Merge PR #12168: [dune] Fix dependencies of refman.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-27Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed ↵Clément Pit-Claudel
in 8.5).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:31:20 +0000