aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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-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-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-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.
2019-07-11Merge PR #10424: Update doc for % escapes in Sphinx, improve error messagesClément Pit-Claudel
Reviewed-by: cpitclaudel
2019-07-11Merge PR #10510: Fixed a few wrong reference and typosThéo Zimmermann
Reviewed-by: Zimmi48
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: ppedrot
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes
2019-07-10Fixed a few wrong reference and typosFlorent Hivert
2019-07-08Adding a changelog.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
Not pretty, but it had to be done some day, as `Globnames` seems to be on the way out. I have taken the opportunity to reduce the number of `open` in the codebase. The qualified style would indeed allow us to use a bit nicer names `GlobRef.Inductive` instead of `IndRef`, etc... once we have the tooling to do large-scale refactoring that could be tried.
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
The changes are large due to `Pervasives` deprecation: - the `Pervasives` module has been deprecated in favor of `Stdlib`, we have opted for introducing a few wrapping functions in `Util` and just unqualified the rest of occurrences. We avoid the shims as in the previous attempt. - a bug regarding partial application have been fixed. - some formatting functions have been deprecated, but previous versions don't include a replacement, thus the warning has been disabled. We may want to clean up things a bit more, in particular w.r.t. modules once we can move to OCaml 4.07 as the minimum required version. Note that there is a clash between 4.08.0 modules `Option` and `Int` and Coq's ones. It is not clear if we should resolve that clash or not, see PR #10469 for more discussion. On the good side, OCaml 4.08.0 does provide a few interesting functionalities, including nice new warnings useful for devs.
2019-07-05Correct doc about default value for Typeclasses Dependency OrderGaëtan Gilbert
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-07-03Merge PR #10419: [api] Refactor most of `Decl_kinds`Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: herbelin
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ↵Kazuhiko Sakaguchi
new one
2019-07-01Update doc for % escapes in Sphinx doc, improve error messagesJim Fehrle
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
We move the bulk of `Decl_kinds` to a better place [namely `interp/decls`] and refactor the use of this information quite a bit. The information seems to be used almost only for `Dumpglob`, so it certainly should end there to achieve a cleaner core. Note the previous commits, as well as the annotations regarding the dubious use of the "variable" data managed by the `Decls` file. IMO this needs more work, but this should be a good start.
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: herbelin Ack-by: jfehrle
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
It prints a goal given its internal goal id and the Stm state id.
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
This looks more principled, and doesn't require as much tinkering with the typing implementation.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 03:11:13 +0000