index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
*
Fix documentation typo (bug #4994).
Guillaume Melquiond
2016-08-04
*
Reference Manual / Extraction: the original example command no longer works w...
Matej Kosik
2016-06-20
*
In Regular Subst Tactic mode, ensure that the order of hypotheses is
Hugo Herbelin
2016-05-03
*
Update tutorial (fix bug #4699).
Guillaume Melquiond
2016-04-28
*
FIX: HTML version of Chapter 4 of the Reference Manual
Matej Kosik
2016-04-12
*
TYPOGRAPHY: adding missing \noindent macros
Matej Kosik
2016-04-12
*
Document Hint Mode, cleanup Hint doc.
Matthieu Sozeau
2016-02-24
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.
Maxime Dénès
2016-01-20
*
Documenting Set Bullet Behavior.
Hugo Herbelin
2016-01-20
*
Clarifying the documentation of tactics "cbv" and "lazy".
Hugo Herbelin
2016-01-20
*
Thanks Hugo, but let's remain factual.
Maxime Dénès
2016-01-15
*
MMaps: remove it from final 8.5 release, since this new library isn't mature ...
Pierre Letouzey
2016-01-13
*
Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.
Hugo Herbelin
2016-01-12
*
Documenting dtauto and dintuition.
Hugo Herbelin
2016-01-12
*
Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".
Hugo Herbelin
2016-01-12
*
Documenting option 'Set Bracketing Last Introduction Pattern'.
Hugo Herbelin
2016-01-12
*
restore documentation of admit
Enrico Tassi
2016-01-12
*
Fix description of command-line options in the manual.
Guillaume Melquiond
2016-01-06
*
Updating credits.
Hugo Herbelin
2015-12-16
*
Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".
Guillaume Melquiond
2015-12-16
*
Proof using: do not clear unused section hyps automatically
Enrico Tassi
2015-12-15
*
Fix \label which was meants to be \ref in doc of CIC terms.
Maxime Dénès
2015-12-14
*
Remove a mention of Set Virtual Machine in doc.
Maxime Dénès
2015-12-14
*
Moved proof_admitted to its own file, named "AdmitAxiom.v".
Maxime Dénès
2015-12-14
*
Extraction: documentation of the new option Unset Extraction SafeImplicits
Pierre Letouzey
2015-12-12
*
Indexing and documenting some options.
Pierre-Marie Pédrot
2015-12-12
*
Remove Set Virtual Machine from doc, since the command itself has been removed.
Maxime Dénès
2015-12-11
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
Refman, ch. 4: A few fixes.
Hugo Herbelin
2015-12-10
*
ENH: redundant examples were removed
Matej Kosik
2015-12-10
*
FIX: wrong reference to a figure
Matej Kosik
2015-12-10
*
CLEANUP: putting examples inside "figure" environment
Matej Kosik
2015-12-10
*
ENH: The definition of the "_ ; _" operation on local context was added.
Matej Kosik
2015-12-10
*
TYPOGRAPHY: adjustments
Matej Kosik
2015-12-10
*
PROPOSITION: the side-condition was made more specific.
Matej Kosik
2015-12-10
*
PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'
Matej Kosik
2015-12-10
*
PROPOSITION: Added an explicit definition of the notation for enriching the g...
Matej Kosik
2015-12-10
*
PROPOSITION: Added "if" and "then" words missing in the original sentence.
Matej Kosik
2015-12-10
*
PROPOSITION: Example was simplified
Matej Kosik
2015-12-10
*
DONE
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
TYPOGRAPHY
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: to do
Matej Kosik
2015-12-10
*
GRAMMAR: added punctuation
Matej Kosik
2015-12-10
[next]