aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-04-22Extend Canonical Structure documentation.Jan-Oliver Kaiser
This commit adds a more detailed explanation of what kinds of terms are allowed in fields of a canonical instance, how the fields are used as keys for canonical extension, what terms are considered overlapping, and how Coq reacts to overlapping fields.
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
Reviewed-by: JasonGross Ack-by: jfehrle
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Zimmi48
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in ↵coqbot-app[bot]
Sphinx output Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-04-17Improve conversion chapter.Jim Fehrle
2021-04-17Disambiguate move tactics.Jim Fehrle
2021-04-17Include (* ... *) comments in .. coqtop:: directives in Sphinx outputJim Fehrle
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence.
2021-04-16[zify] bugfixFrederic Besson
- to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-10Merge PR #14091: Fix link in doc/cic.rst, there is no Credits chapter anymorecoqbot-app[bot]
Reviewed-by: jfehrle
2021-04-10Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on ↵coqbot-app[bot]
red/orange background) Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-04-10Fix link in doc/cic.rst, there is no Credits chapter anymoreYannick Forster
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
Fixes #14092: Print Grammar ltac2 should exist.
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-01Merge PR #14044: [RM] changelog for 8.13.2coqbot-app[bot]
Reviewed-by: Zimmi48
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-30Remove the :> type castJim Fehrle
2021-03-29[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0Emilio Jesus Gallego Arias
Fixes #10704
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2021-03-13Documenting the changes.Pierre-Marie Pédrot
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: jfehrle
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-03-04[doc] Set/Unset Printing Raw LiteralsEnrico Tassi
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ↵coqbot-app[bot]
raised. Reviewed-by: jfehrle
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
2021-02-28Fix link of default_bindings.slb Prime
2021-02-27Remove decimal-only number notationsPierre Roux
This was deprecated in 8.12
2021-02-26Signed primitive integersAna
Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22changelog for 8.13.1Enrico Tassi
2021-02-14Show "Error:"/"Warning:" with white type (on red/orange background)Jim Fehrle
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-02-05Fix hierarchy of sections in module chapter.Théo Zimmermann
2021-01-28Merge PR #13799: Replace : term with : type in open binders.coqbot-app[bot]
Reviewed-by: jfehrle
2021-01-28Merge PR #13789: Document limitation of rewrite regarding occurrence selection.coqbot-app[bot]
Reviewed-by: jfehrle Reviewed-by: silene
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:53:30 +0000