index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
/
addendum
Age
Commit message (
Expand
)
Author
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-08
Merge PR #11050: Replace "option" in doc when it refers to a flag
Théo Zimmermann
2019-11-06
Replace "option" in doc when it refers to a flag
Jim Fehrle
2019-11-04
Cite POPL19 SProp paper
Gaëtan Gilbert
2019-11-03
Elan → Stratego in documentation of `rewrite_strat`.
Robbert Krebbers
2019-11-01
Update the deprecation doc of `Shrink Obligations`
Jason Gross
2019-10-14
Merge PR #10811: Allow SProp default on
Pierre-Marie Pédrot
2019-10-04
Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...
Pierre-Marie Pédrot
2019-10-04
Allow SProp default on
Gaëtan Gilbert
2019-10-03
Improved handling of micromega caches
Frédéric Besson
2019-10-02
Loosen restrictions on mixing universe mono/polymorphism in sections
Gaëtan Gilbert
2019-09-25
Adding documentation for the move of sections data to kernel.
Pierre-Marie Pédrot
2019-09-16
Re-implementation of zify
Frédéric Besson
2019-08-23
[doc] Fix documentation of schedule-vio
Emilio Jesus Gallego Arias
2019-07-22
Merge PR #10441: Attach the universe polymorphic status to sections.
Gaëtan Gilbert
2019-07-18
[doc] Fix typo in doc/sphinx/addendum/ring.rst
Wojciech Nawrocki
2019-07-18
Adding changelog and documentation.
Pierre-Marie Pédrot
2019-07-05
Correct doc about default value for Typeclasses Dependency Order
Gaëtan Gilbert
2019-07-02
Improve the ambiguous paths warning to indicate which path is ambiguous with ...
Kazuhiko Sakaguchi
2019-06-04
[rewrite] Add Morphism syntax made different for module type parameters
Enrico Tassi
2019-05-24
Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Emilio Jesus Gallego Arias
2019-05-23
do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Georges Gonthier
2019-05-23
Define many undefined tokens, and other misc fixes.
Théo Zimmermann
2019-05-22
[refman] Add more missing @ signs
Clément Pit-Claudel
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-19
Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ...
Théo Zimmermann
2019-05-16
[refman] Introduce syntax for alternatives in notations
Clément Pit-Claudel
2019-05-10
[Attributes] Allow explicit value for two-valued attributes
Vincent Laporte
2019-05-10
[User manual] Fix two warnings related to canonical structures
Vincent Laporte
2019-05-02
Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions
Maxime Dénès
2019-04-30
First fixing pass, and experiment with dune-style PR number and author listing.
Théo Zimmermann
2019-04-27
Minor doc improvement.
Théo Zimmermann
2019-04-27
[refman] Fix typo.
Théo Zimmermann
2019-04-16
Update and fix documentation of Program Fixpoint with measure
Maxime Dénès
2019-04-10
Improve SProp error message to mention the Allow StrictProp flag.
Théo Zimmermann
2019-03-30
[Manual] Typo
Vincent Laporte
2019-03-29
typo in ring.rst
thery
2019-03-28
Merge PR #9743: Relax the ambiguous path condition of coercion
Enrico Tassi
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-25
Remove `Automatic Coercions Import` option.
Maxime Dénès
2019-03-18
Update doc and changes
Kazuhiko Sakaguchi
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
[prev]
[next]