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
2020-04-21
Adding a Declare ML Module in empty file Ltac.v.
Hugo Herbelin
2020-04-21
Change log.
Hugo Herbelin
2020-04-21
Document changed warnings and erros following #12038.
Théo Zimmermann
2020-04-21
Update common.edit_mlg and fullGrammar following #12038.
Théo Zimmermann
2020-04-21
Move documentation on Funind into a single file.
Théo Zimmermann
2020-04-21
Merge all documentation on Funind into the same file.
Théo Zimmermann
2020-04-21
Consolidate funind tactics and Functional Scheme in Funind section of the Lib...
Théo Zimmermann
2020-04-21
Extract funind tactics to funind section of the Libraries chapter.
Théo Zimmermann
2020-04-21
Remove parts of the Tactics chapter.
Théo Zimmermann
2020-04-21
Remove parts of the Tactics chapter.
Théo Zimmermann
2020-04-21
Remove everything in the Tactics chapter up-to function induction and a bit b...
Théo Zimmermann
2020-04-21
Merge PR #12060: CoqIDE: Disable client-side decoration on Windows
Pierre-Marie Pédrot
2020-04-21
Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom...
Pierre-Marie Pédrot
2020-04-21
Merge PR #12014: [stdlib] Add properties of operations on vectors
Hugo Herbelin
2020-04-21
Merge PR #11883: Fix #7812: autounfold's behavior depends on file names
Hugo Herbelin
2020-04-20
[refman] Remove references to omega from Tactics chapter.
Théo Zimmermann
2020-04-20
Merge PR #12126: TIMEFMT: Display the output file name
Gaëtan Gilbert
2020-04-20
Adding change log for PR #12026 (definitions in coqdoc link to themselves).
Hugo Herbelin
2020-04-20
TIMEFMT: Display the output file name
Jason Gross
2020-04-20
Remove funind tactics from Tactics chapter.
Théo Zimmermann
2020-04-20
Remove Functional Scheme from Scheme chapter.
Théo Zimmermann
2020-04-20
Move Functional Scheme to Funind section.
Théo Zimmermann
2020-04-20
Extract Functional Scheme from Scheme chapter.
Théo Zimmermann
2020-04-20
Remove coqremote stylesheets which were useless since the Sphinx migration.
Théo Zimmermann
2020-04-20
Remove probably useless doc/sphinx/coqdoc.css.
Théo Zimmermann
2020-04-20
Adding change log.
Hugo Herbelin
2020-04-20
Merge PR #12123: Don't create index entries for the name "_"
Théo Zimmermann
2020-04-20
Change log for PR #12045.
Hugo Herbelin
2020-04-20
Merge PR #12106: Coqide: Apply style scheme and language settings to the thre...
Pierre-Marie Pédrot
2020-04-19
added changelog for PR 12044
ilya
2020-04-19
A library on cyclic permutations: CPermutation
Olivier Laurent
2020-04-19
Don't create index entries for the name "_"
Jim Fehrle
2020-04-19
Merge PR #12033: Let coqdoc be informed by coq about binding variables (incid...
Lysxia
2020-04-19
CoqIDE: Adding a short documentation on style/theme customization.
Hugo Herbelin
2020-04-19
remove useless hypothesis in NoDup_Permutation_bis
Olivier Laurent
2020-04-17
Coqide: Apply style scheme and language to the three buffers.
Hugo Herbelin
2020-04-17
Deprecate “omega”
Vincent Laporte
2020-04-17
ZArith: move lia hints to a dedicated module
Vincent Laporte
2020-04-17
Merge PR #11963: NativeCompute Timing: Use real, not user time
Pierre-Marie Pédrot
2020-04-17
Merge PR #11972: Fix require in section
Pierre-Marie Pédrot
2020-04-16
NativeCompute Timing: Use real, not user time
Jason Gross
2020-04-16
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Gaëtan Gilbert
2020-04-16
Merge PR #12070: Ignore -native-compiler option when disabled
Pierre-Marie Pédrot
2020-04-16
Merge PR #11861: [declare] [rewrite] Use high-level declare API
Pierre-Marie Pédrot
2020-04-16
CoqIDE: Disable client-side decoration on Windows
Attila Gáspár
2020-04-15
Adding change log for PR #12033 (hyperlinks on binders for coqdoc).
Hugo Herbelin
2020-04-15
[declare] Rename `Declare.t` to `Declare.Proof.t`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Merge `Proof_global` into `Declare`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Move proof_global functionality to Proof_global from Pfedit
Emilio Jesus Gallego Arias
2020-04-15
Ignore -native-compiler option when disabled
Pierre Roux
[prev]
[next]