aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum/implicit-coercions.rst
AgeCommit message (Collapse)Author
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-03-09Remove some productionlistsJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
This change improves the relaxed ambiguous path condition of coercions (#9743) to check that any circular inheritance path of `C >-> C` is definitionally equal to the identity function of the class `C`. Moreover, for a new inheritance path `p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not report the ambiguity of `p` and `q` if they have a common element, that is to say: `p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2` for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`. In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be checked; thus, checking the ambiguity of `p` and `q` is redundant with them. If the new mechanism does not report any ambiguous path, the inheritance graph must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]: 1. for any circular path `p : C >-> C`, `p` is definitionally equal to the identity function, and 2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible. [Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95, LNCS, vol 1158, Springer, 1996, pp 1-15. [Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance, In: POPL '97, ACM, 1997, pp 292-301.
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ↵Kazuhiko Sakaguchi
new one
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Ack-by: pi8027
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
This option made the Coercions command follow non-standard scoping rules (effect on `Require` rather than `Import`). It was already marked for deletion in 8.8.
2019-03-18Update doc and changesKazuhiko Sakaguchi
2019-02-11Small typos in the documentation.Martin Bodin
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try ↵Théo Zimmermann
to fix all misuses.
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
And a few more Sphinx fixes in passing.
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter.
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
This warning makes it much easier to stop relying on `Set Automatic Coercions Import`. Tested with success on math-classes.
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the ↵Zeimer
Reference Manual.
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
Co-Authored-By: @Zimmi48
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
In particular, remove trailing dots.
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
All the error messages start with a capitalized letter and end with a dot.
2018-05-05Fix typo in Coercions chapter.Théo Zimmermann
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-16[Sphinx] Fix a lot of references and description of optionsMaxime Dénès
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14[sphinx] Fix many warnings.Théo Zimmermann
Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
2018-03-29[Sphinx] Add chapter 18Maxime Dénès
Thanks to Pierre Letouzey for porting this chapter.
2018-03-29[Sphinx] Move chapter 18 to new infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:07:17 +0000