aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Fix a really small doc typoGravatar Ricky Elrod2016-05-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\|
| * Update tutorial (fix bug #4699).Gravatar Guillaume Melquiond2016-04-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
| * TYPOGRAPHY: adding missing \noindent macrosGravatar Matej Kosik2016-04-12
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | |/ | |/|
| * | Document Hint Mode, cleanup Hint doc.Gravatar Matthieu Sozeau2016-02-24
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | 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
* | | Updating and improving the documentation of intros patterns.Gravatar Hugo Herbelin2016-01-14
| * | MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-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
* | | TYPOGRAPHY: correction of one particular error in the Reference ManualGravatar Matej Kosik2015-12-18
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\| |
| * | 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
* | | Simplifying documentation of "assert form as pat".Gravatar Hugo Herbelin2015-12-15
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-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
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\| |
| * | 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