aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2019-09-10Fixing coqide doc about location of "coqiderc" and "coqide.bindings".Hugo Herbelin
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2019-09-05Merge PR #10731: Ocfnash/stdlib additionsHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2019-09-05Merge PR #10730: Add missing index for From ... Require ...Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-09-04Add changelog entry for 10731Oliver Nash
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-09-03Apply suggestions from code reviewOliver Nash
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-09-03New lemmas for List.vOliver Nash
* filter_app (moved from MSets/MSetRBT.v) * filter_map * filter_ext_in * ext_in_filter * filter_ext_in_iff * filter_ext * concat_filter_map * combine_nil * combine_firstn_l * combine_firstn_r * combine_firstn * nodup_fixed_point
2019-09-01edits per reviewYishuai Li
2019-09-01Changelog: more accurate on unconsYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages.
2019-08-25Merge PR #10632: Prove the completeness of real numbers from logical axiom ↵Hugo Herbelin
sig_not_dec Reviewed-by: herbelin
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
This improves error reporting. Addendum to #10515
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
Master version of the fix for #10679
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-09Add a changelog entryKazuhiko Sakaguchi
Acknowledgement: This work is financially supported by Peano System Inc. on-behalf-of: @peano-system <info@peano-system.jp>
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵Maxime Dénès
involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ↵Vincent Semeria
Cauchy reals
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive ↵Théo Zimmermann
Projection Compatibility Reviewed-by: Zimmi48
2019-08-05Merge PR #10608: Copy edit the Ltac2 documentationJim Fehrle
Reviewed-by: jfehrle Reviewed-by: ppedrot
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
Ack-by: Zimmi48 Ack-by: silene
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-29Document changes by PR 10324Vincent Laporte
White spaces are forbidden in the “&ident” syntax for ltac2 references.
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel Ack-by: herbelin
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
Reviewed-by: ejgallego Reviewed-by: gares
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one ↵Guillaume Melquiond
complained (fixes #10580).
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
It has been deprecated since 8.4. The documentation was incorrect since at least 8.5 (the last two arguments were ignored). `Backtrack m n p` was a synonym for `BackTo m` We also move `BackTo` handling to coqtop, since it is not meant to be part of the document.
2019-07-23doc: Fix a detail in 2 files describing the under tacticErik Martin-Dorel
href: coq/coq#9651
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are implemented in the kernel so that they can be used by OCaml code (e.g., extracted code) as the other primitives.
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel).
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: mattam82
2019-07-20Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg ↵Théo Zimmermann
files and insert it into .rst files Ack-by: Zimmi48 Ack-by: gares Ack-by: ppedrot
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
and inserting it into the .rst files
2019-07-18Shorten changelogVincent Semeria
2019-07-18[doc] Fix typo in doc/sphinx/addendum/ring.rstWojciech Nawrocki
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-17Rename ConstructiveRIneq and ConstructiveRcompleteVincent Semeria
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. ↵Vincent Semeria
Redefine classical real numbers as a quotient of those constructive real numbers.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:58:36 +0000