aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
* Reference Manual / Extraction: the original example command no longer works w...Gravatar Matej Kosik2016-06-20
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* Update tutorial (fix bug #4699).Gravatar Guillaume Melquiond2016-04-28
* FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
* TYPOGRAPHY: adding missing \noindent macrosGravatar Matej Kosik2016-04-12
* Document Hint Mode, cleanup Hint doc.Gravatar Matthieu Sozeau2016-02-24
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Gravatar Maxime Dénès2016-01-20
* Documenting Set Bullet Behavior.Gravatar Hugo Herbelin2016-01-20
* Clarifying the documentation of tactics "cbv" and "lazy".Gravatar Hugo Herbelin2016-01-20
* Thanks Hugo, but let's remain factual.Gravatar Maxime Dénès2016-01-15
* MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Gravatar Hugo Herbelin2016-01-12
* Documenting dtauto and dintuition.Gravatar Hugo Herbelin2016-01-12
* Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Gravatar Hugo Herbelin2016-01-12
* Documenting option 'Set Bracketing Last Introduction Pattern'.Gravatar Hugo Herbelin2016-01-12
* restore documentation of admitGravatar Enrico Tassi2016-01-12
* Fix description of command-line options in the manual.Gravatar Guillaume Melquiond2016-01-06
* Updating credits.Gravatar Hugo Herbelin2015-12-16
* Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* Fix \label which was meants to be \ref in doc of CIC terms.Gravatar Maxime Dénès2015-12-14
* Remove a mention of Set Virtual Machine in doc.Gravatar Maxime Dénès2015-12-14
* Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14
* Extraction: documentation of the new option Unset Extraction SafeImplicitsGravatar Pierre Letouzey2015-12-12
* Indexing and documenting some options.Gravatar Pierre-Marie Pédrot2015-12-12
* Remove Set Virtual Machine from doc, since the command itself has been removed.Gravatar Maxime Dénès2015-12-11
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* Refman, ch. 4: A few fixes.Gravatar Hugo Herbelin2015-12-10
* ENH: redundant examples were removedGravatar Matej Kosik2015-12-10
* FIX: wrong reference to a figureGravatar Matej Kosik2015-12-10
* CLEANUP: putting examples inside "figure" environmentGravatar Matej Kosik2015-12-10
* ENH: The definition of the "_ ; _" operation on local context was added.Gravatar Matej Kosik2015-12-10
* TYPOGRAPHY: adjustmentsGravatar Matej Kosik2015-12-10
* PROPOSITION: the side-condition was made more specific.Gravatar Matej Kosik2015-12-10
* PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'Gravatar Matej Kosik2015-12-10
* PROPOSITION: Added an explicit definition of the notation for enriching the g...Gravatar Matej Kosik2015-12-10
* PROPOSITION: Added "if" and "then" words missing in the original sentence.Gravatar Matej Kosik2015-12-10
* PROPOSITION: Example was simplifiedGravatar Matej Kosik2015-12-10
* DONEGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* TYPOGRAPHYGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: to doGravatar Matej Kosik2015-12-10
* GRAMMAR: added punctuationGravatar Matej Kosik2015-12-10