index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
Commit message (
Expand
)
Author
Age
*
Fix typo in the refman.
Théo Zimmermann
2017-12-19
*
Merge PR #6381: A version of [time] that works on constr evaluation
Maxime Dénès
2017-12-18
|
\
*
\
Merge PR #6380: Add tactics to reset and display the Ltac profile
Maxime Dénès
2017-12-18
|
\
\
*
\
\
Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...
Maxime Dénès
2017-12-18
|
\
\
\
*
|
|
|
[doc] Nit on the manual.
Emilio Jesus Gallego Arias
2017-12-17
*
|
|
|
Merge PR #6219: Document undocumented options
Maxime Dénès
2017-12-15
|
\
\
\
\
|
|
|
|
*
Add documentation for time_constr
Jason Gross
2017-12-14
|
|
|
|
/
|
|
|
*
Add doc+changelog entries for new LtacProf tactics
Jason Gross
2017-12-14
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...
Maxime Dénès
2017-12-14
|
\
\
\
*
\
\
\
Merge PR #6169: Clean up/deprecated options
Maxime Dénès
2017-12-14
|
\
\
\
\
|
|
|
*
|
Document Short Module Printing.
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Document Rewriting Schemes (quickly).
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Document Record Elimination Schemes.
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Document Asymmetric Patterns.
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Document some omega options (missing Omega Oldstyle).
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Add doc for Set Debug RAKAM.
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Add doc for Set Debug Cbv.
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Add doc for Set Info/Debug Auto/Trivial/Eauto.
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Add optindex for Set Bullet Behavior.
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Add doc for Set Congruence Verbose
Gaëtan Gilbert
2017-12-14
|
|
|
*
|
Fix typo in doc optindex for Typeclass Resolution ...
Gaëtan Gilbert
2017-12-14
|
|
*
|
|
Documenting the new options for printing "match".
Hugo Herbelin
2017-12-12
|
*
|
|
|
Remove deprecated appcontext and corresponding documentation.
Théo Zimmermann
2017-12-11
|
|
/
/
/
*
|
|
|
[make] remove unneeded generated file "tolink.ml"
Emilio Jesus Gallego Arias
2017-12-10
*
|
|
|
[build] Remove coqmktop in favor of ocamlfind.
Emilio Jesus Gallego Arias
2017-12-10
|
/
/
/
*
|
|
Merge PR #6277: Qualified import in coqchk
Maxime Dénès
2017-12-07
|
\
\
\
|
|
|
*
use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language
Paul Steckler
2017-12-05
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #890: Global universe declarations
Maxime Dénès
2017-12-05
|
\
\
\
*
\
\
\
Merge PR #6300: Clarify operation of sequences, fixes #6095
Maxime Dénès
2017-12-05
|
\
\
\
\
*
\
\
\
\
Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212
Maxime Dénès
2017-12-05
|
\
\
\
\
\
|
|
*
|
|
|
clarify operation of sequences, #6095
Paul Steckler
2017-12-01
|
|
|
*
|
|
[refman] Expand a little on global universes.
Matthieu Sozeau
2017-12-01
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
*
|
Documenting the -Q flag of coqchk.
Pierre-Marie Pédrot
2017-12-01
*
|
|
|
|
Merge PR #6276: Coqchk accepts filenames
Maxime Dénès
2017-12-01
|
\
\
\
\
\
|
|
_
|
/
/
/
|
/
|
|
/
/
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Documenting the possibility to pass filenames to coqchk.
Pierre-Marie Pédrot
2017-11-29
|
|
|
/
|
|
/
|
|
|
*
use \ocaml macro in new text
Paul Steckler
2017-11-28
*
|
|
Fix (partial) #4878: option to stop autodeclaring axiom as instance.
Gaëtan Gilbert
2017-11-28
|
/
/
*
|
Allow local universe renaming in Print.
Gaëtan Gilbert
2017-11-25
|
*
use OCaml criteria for infix ops, #6212
Paul Steckler
2017-11-22
|
/
*
Rename coq-inferior.el -> inferior-coq.el to match provided feature.
Gaëtan Gilbert
2017-11-19
*
coq_makefile: document COQ_SRC_SUBDIRS
Enrico Tassi
2017-11-13
*
Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",
Samuel Gruetter
2017-11-06
*
Merge PR #1139: Add a linter.
Maxime Dénès
2017-11-06
|
\
*
\
Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631
Maxime Dénès
2017-10-27
|
\
\
*
|
|
Rename \Tree to \NatTree
Johannes Kloos
2017-10-25
|
|
*
Put newlines at the end of files.
Gaëtan Gilbert
2017-10-25
*
|
|
Fix #5763: Strictly positive example is out of order.
jkloos
2017-10-24
|
*
|
Fix #4846
Johannes Kloos
2017-10-24
|
*
|
Fix #5413: [unfold ... in] not documented
Johannes Kloos
2017-10-24
|
*
|
Documentation: Add various basic constructs to the index.
Johannes Kloos
2017-10-24
[next]