index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
/
addendum
/
type-classes.rst
Age
Commit message (
Expand
)
Author
2021-03-08
Convert 2nd part of rewriting chapter to prodn
Jim Fehrle
2020-12-30
Convert rewriting and proof-mode chapters to prodn
Jim Fehrle
2020-11-24
Convert auto chapter to prodn
Jim Fehrle
2020-11-20
Use nat_or_var where negative values don't make sense
Jim Fehrle
2020-11-18
[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.
Emilio Jesus Gallego Arias
2020-11-16
Merge PR #13188: Default disable automatic generalization of Instance type
Pierre-Marie Pédrot
2020-11-15
Doc and changelog for Instance Generalized Output
Gaëtan Gilbert
2020-11-14
Distinguish one_pattern and one_term nonterminals
Jim Fehrle
2020-11-09
[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.
Théo Zimmermann
2020-10-24
Convert misc chapters to prodn
Jim Fehrle
2020-10-20
Add some missing smallcaps.
Théo Zimmermann
2020-09-27
Reduce nitpick_ignore list a little.
Théo Zimmermann
2020-09-11
[refman] Rename num to natural
Pierre Roux
2020-04-26
Convert syntax extensions chapter to prodn
Jim Fehrle
2020-03-19
Document all the existing attributes.
Théo Zimmermann
2020-03-13
Implementing postponed constraints in TC resolution
Matthieu Sozeau
2020-02-28
Convert Gallina Vernac to use prodn
Jim Fehrle
2019-11-29
Remove deprecated Typeclasses Axioms Are Instances.
Théo Zimmermann
2019-11-20
Merge PR #11119: 8.10-backportable part of #10575
Clément Pit-Claudel
2019-11-14
Restore documentation of `Typeclasses Axioms Are Instances`
Maxime Dénès
2019-11-13
Return of Refine Instance as an attribute.
Gaëtan Gilbert
2019-11-06
Replace "option" in doc when it refers to a flag
Jim Fehrle
2019-07-05
Correct doc about default value for Typeclasses Dependency Order
Gaëtan Gilbert
2019-05-21
Fixing typos - Part 1
JPR
2019-05-20
Remove Refine Instance Mode option
Maxime Dénès
2019-05-19
[refman] Fix up the documentation of Instance and Existing Instance
Clément Pit-Claudel
2019-05-19
[refman] Misc fixes (indentation, whitespace, notation syntax)
Clément Pit-Claudel
2019-05-16
[refman] Introduce syntax for alternatives in notations
Clément Pit-Claudel
2019-05-02
Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions
Maxime Dénès
2019-04-27
Minor doc improvement.
Théo Zimmermann
2019-04-27
[refman] Fix typo.
Théo Zimmermann
2019-03-27
Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.
Jim Fehrle
2019-03-27
Deprecate `Refine Instance Mode` option
Maxime Dénès
2019-03-26
Fix syntax of Typeclasses eauto := in reference manual.
Théo Zimmermann
2019-03-18
[Manual] Move command Context after Let, and more polishing
Lysxia
2019-03-17
[Manual] Move doc on Let into Section mechanism, and more polishing
Lysxia
2019-03-17
[Manual] Gather section-specific commands in Section documentation (fix #9704)
Lysxia
2019-03-17
[Manual] Improve chapter Type classes, and add mention of Context under Variable
Lysxia
2019-02-18
Fix doc for Refine Instance Mode
Gaëtan Gilbert
2019-02-18
Fix failing coqtops in type-classes.rst
Gaëtan Gilbert
2018-12-04
Add undocumented options from mattam82
Jim Fehrle
2018-12-04
Document undocumented flags and options
Jim Fehrle
2018-11-30
Add indexes for coercion / substructure symbol :>.
Théo Zimmermann
2018-11-27
[Typeclasses] Warn when RHS of `:>` is not a class
Vincent Laporte
2018-11-21
[sphinx] Progress towards closing #7602: remove most objects without a body.
Théo Zimmermann
2018-09-20
Rewrite "Flags, Options and Tables" section.
Jim Fehrle
2018-09-20
[doc] Include the rst and LaTeX preambles automatically in all files
Clément Pit-Claudel
2018-08-31
Fixed the seealso directive in a few places.
Zeimer
2018-08-31
Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...
Zeimer
2018-08-01
Improved grammar and spelling in chapters 'Type Classes', 'Omega' and 'Microm...
Zeimer
[next]