aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-28Update tutorial (fix bug #4699).Guillaume Melquiond
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-12FIX: HTML version of Chapter 4 of the Reference ManualMatej Kosik
2016-04-12TYPOGRAPHY: adding missing \noindent macrosMatej Kosik
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-24Document Hint Mode, cleanup Hint doc.Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-20Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Maxime Dénès
2016-01-20Documenting Set Bullet Behavior.Hugo Herbelin
2016-01-20Clarifying the documentation of tactics "cbv" and "lazy".Hugo Herbelin
2016-01-15Thanks Hugo, but let's remain factual.Maxime Dénès
2016-01-14Updating and improving the documentation of intros patterns.Hugo Herbelin
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Hugo Herbelin
2016-01-12Documenting dtauto and dintuition.Hugo Herbelin
2016-01-12Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Hugo Herbelin
2016-01-12Documenting option 'Set Bracketing Last Introduction Pattern'.Hugo Herbelin
2016-01-12restore documentation of admitEnrico Tassi
2016-01-06Fix description of command-line options in the manual.Guillaume Melquiond
2015-12-18TYPOGRAPHY: correction of one particular error in the Reference ManualMatej Kosik
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-16Updating credits.Hugo Herbelin
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Simplifying documentation of "assert form as pat".Hugo Herbelin
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Fix \label which was meants to be \ref in doc of CIC terms.Maxime Dénès
2015-12-14Remove a mention of Set Virtual Machine in doc.Maxime Dénès
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-12-12Extraction: documentation of the new option Unset Extraction SafeImplicitsPierre Letouzey
2015-12-12Indexing and documenting some options.Pierre-Marie Pédrot
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Remove Set Virtual Machine from doc, since the command itself has been removed.Maxime Dénès
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-10Refman, ch. 4: A few fixes.Hugo Herbelin
2015-12-10ENH: redundant examples were removedMatej Kosik
2015-12-10FIX: wrong reference to a figureMatej Kosik
2015-12-10CLEANUP: putting examples inside "figure" environmentMatej Kosik
2015-12-10ENH: The definition of the "_ ; _" operation on local context was added.Matej Kosik
2015-12-10TYPOGRAPHY: adjustmentsMatej Kosik
2015-12-10PROPOSITION: the side-condition was made more specific.Matej Kosik
2015-12-10PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'Matej Kosik
2015-12-10PROPOSITION: Added an explicit definition of the notation for enriching the g...Matej Kosik
2015-12-10PROPOSITION: Added "if" and "then" words missing in the original sentence.Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 12:08:28 +0000