index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
Age
Commit message (
Expand
)
Author
2020-03-27
Remove the part about coqdoc from the utilities chapter.
Théo Zimmermann
2020-03-27
Prepare split of section about coqdoc.
Théo Zimmermann
2020-03-26
Merge PR #11929: Reintroduce a command that was actually used in another one....
Clément Pit-Claudel
2020-03-26
Reintroduce commands that were actually used. Fix build of PDF manual.
Théo Zimmermann
2020-03-26
Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.
Théo Zimmermann
2020-03-26
CIC is printed in all-caps.
Théo Zimmermann
2020-03-26
Removing deprecated destruct syntax _eqn.
Hugo Herbelin
2020-03-26
Shrink refman-prelude files.
Théo Zimmermann
2020-03-26
Remove outdated mention of -allow-sprop.
Théo Zimmermann
2020-03-26
Print a warning when parsing non floating-point values.
Pierre Roux
2020-03-25
Doc_grammar: Update cmd:: and tacn:: constructs in .rsts
Jim Fehrle
2020-03-25
Convert Gallina Extensions to use prodn
Jim Fehrle
2020-03-24
Merge PR #11892: [refman] Fix caching, which was broken by the addition of co...
Théo Zimmermann
2020-03-23
[refman] Fix caching, which was broken by the addition of coq_config
Clément Pit-Claudel
2020-03-21
Reorder the load/require cmd-options and set/unset cmd-options
Lasse Blaauwbroek
2020-03-20
Add an index for attributes.
Théo Zimmermann
2020-03-20
Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.
Pierre-Marie Pédrot
2020-03-20
Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yes
Enrico Tassi
2020-03-19
Merge PR #11601: [refman] Move chapters into new structure.
Clément Pit-Claudel
2020-03-19
Merge PR #11862: Fix deprecation warning in sphinx and remove workaround for ...
Théo Zimmermann
2020-03-19
[refman] Remove workaround for sphinx-doc/sphinx#4983
Clément Pit-Claudel
2020-03-19
Interpret the Export modifier of Set and Unset as an attribute.
Théo Zimmermann
2020-03-19
Document all the existing attributes.
Théo Zimmermann
2020-03-19
Adapt to sub-TOC not showing in PDF output.
Théo Zimmermann
2020-03-19
[refman] Move chapters into new structure.
Théo Zimmermann
2020-03-19
firstorder: default tactic is “auto with core”
Vincent Laporte
2020-03-18
Merge PR #11559: Remove year in headers.
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-18
Add documentation for the export hint.
Pierre-Marie Pédrot
2020-03-16
Merge PR #11813: Fixed link to "match" syntax figures.
Théo Zimmermann
2020-03-16
Document coq_makefile behavior wrt -native-compiler yes
Pierre Roux
2020-03-13
Implementing postponed constraints in TC resolution
Matthieu Sozeau
2020-03-12
Update doc/sphinx/addendum/extended-pattern-matching.rst
larsr
2020-03-12
Fixed link to "match" syntax.
larsr
2020-03-09
Remove some productionlists
Jim Fehrle
2020-03-08
[doc] [dune] Update Dune build instructions
Emilio Jesus Gallego Arias
2020-03-05
Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.
Maxime Dénès
2020-03-05
Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...
Pierre-Marie Pédrot
2020-03-04
Adding support for an "only parsing" modifier in "where"-based notations.
Hugo Herbelin
2020-03-03
[loadpath] Rework and simplify ML loadpath handling
Emilio Jesus Gallego Arias
2020-03-03
Adding an alias "pose proof (x:=a)" for "pose proof a as x".
Hugo Herbelin
2020-02-29
Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.
Clément Pit-Claudel
2020-02-28
Merge PR #11423: Convert Vernacular section of gallina chapter to use prodn
Théo Zimmermann
2020-02-28
Convert Gallina Vernac to use prodn
Jim Fehrle
2020-02-28
Adapt the documentation after deprecation of term hints.
Pierre-Marie Pédrot
2020-02-27
Merge PR #11650: Set Printing Parens
Emilio Jesus Gallego Arias
2020-02-27
Fix #11696: link from refman to stdlib doc is dead.
Théo Zimmermann
2020-02-24
Make it clear how to import Ltac2
Clément Pit-Claudel
2020-02-24
added sphinx doc
Abhishek Anand (optiplex7010@home)
2020-02-23
Merge PR #11120: Refactoring code for application printing + fixing #11091 (i...
Emilio Jesus Gallego Arias
[prev]
[next]