index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2019-01-08
Integrate plugin tutorial after code import
Gaëtan Gilbert
2019-01-08
plugin_tutorial: ignore Coqlib.find_reference deprecation warning.
Gaëtan Gilbert
2019-01-08
Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e...
Gaëtan Gilbert
2019-01-08
Add doc for auto-template warning
Gaëtan Gilbert
2018-12-26
[dune] Build refman with fatal warnings by default like in the Makefile build.
Théo Zimmermann
2018-12-21
Merge PR #9247: Fix typo in gallina specification language doc
Théo Zimmermann
2018-12-19
[doc] typo
Enrico Tassi
2018-12-19
Fix typo in gallina specification language doc
yudetamago
2018-12-18
[ssr] make > a stand alone intro pattern
Enrico Tassi
2018-12-18
[ssr] extended intro patterns: + > [^] /ltac:
Enrico Tassi
2018-12-14
Merge PR #9073: [sphinx] No more undocumented objects.
Clément Pit-Claudel
2018-12-14
Merge PR #9147: [dune] [doc] Support for building the reference manual with D...
Théo Zimmermann
2018-12-14
Turn warning on for undocumented objects. Closes #7602.
Théo Zimmermann
2018-12-14
Fix the SSReflect chapter regarding objects without bodies.
Théo Zimmermann
2018-12-14
Do not raise object without body warning for prodn objects.
Théo Zimmermann
2018-12-13
Merge PR #9211: Fixing incorrect mention of coercions as being part of the in...
Théo Zimmermann
2018-12-13
[dune] [doc] Support for building the reference manual with Dune.
Emilio Jesus Gallego Arias
2018-12-13
Merge PR #9196: Document the deprecation of hint declaration withou database ...
Maxime Dénès
2018-12-12
Fixing incorrect mention of coercions as being part of the interning phase.
Hugo Herbelin
2018-12-12
Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`
Hugo Herbelin
2018-12-11
Add missing formatting.
Théo Zimmermann
2018-12-11
Document the deprecation of hint declaration withou database in refman.
Théo Zimmermann
2018-12-04
Add undocumented options from mattam82
Jim Fehrle
2018-12-04
Document undocumented flags and options
Jim Fehrle
2018-12-04
Giving to type_scope a softer role in printing.
Hugo Herbelin
2018-12-04
Printing priority to most recent notation in case of non-open scopes with delim.
Hugo Herbelin
2018-12-04
Documentation of the rules for printing notations depending on scopes.
Hugo Herbelin
2018-12-03
[sphinx] Same rendering for :n:`@token` and :token:`token`.
Théo Zimmermann
2018-12-03
A few fixes of unexisting tokens.
Théo Zimmermann
2018-12-03
Closes #9118: single backticks are made equivalent to double backticks; try t...
Théo Zimmermann
2018-11-30
Merge PR #9105: Add indexes for coercion / substructure symbol :>.
Clément Pit-Claudel
2018-11-30
Add indexes for coercion / substructure symbol :>.
Théo Zimmermann
2018-11-28
Fix numeral notations doc by indenting
Jason Gross
2018-11-28
Fix string notation doc
Jason Gross
2018-11-28
Add `String Notation` vernacular like `Numeral Notation`
Jason Gross
2018-11-28
Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a class
Matthieu Sozeau
2018-11-27
Merge PR #8850: Private universes for opaque polymorphic constants.
Matthieu Sozeau
2018-11-27
[Typeclasses] Warn when RHS of `:>` is not a class
Vincent Laporte
2018-11-25
Merge PR #9036: Add bodies to sphinx objects.
Clément Pit-Claudel
2018-11-23
Doc for Private Polymorphic Universes.
Gaëtan Gilbert
2018-11-21
[sphinx] Progress towards closing #7602: remove most objects without a body.
Théo Zimmermann
2018-11-19
Minor update to micromega.rst
soraros
2018-11-19
Typo: comment does not match code
Olivier Laurent
2018-11-19
Merge PR #9001: [options] Remove deprecated option automatic introduction.
Pierre-Marie Pédrot
2018-11-19
Merge PR #8451: Print Universes Subgraph
Pierre-Marie Pédrot
2018-11-18
[options] Remove deprecated option automatic introduction.
Emilio Jesus Gallego Arias
2018-11-16
Print Universes Subgraph
Gaëtan Gilbert
2018-11-16
Remove the implicit tactic feature following #7229.
Pierre-Marie Pédrot
2018-11-16
Merge PR #8888: Proof runcountable rebase
Hugo Herbelin
2018-11-07
[doc] also scan plugins/ to build the lirbary index
Enrico Tassi
[prev]
[next]