aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\
* | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
* | typoGravatar Matej Kosik2016-06-07
* | typographyGravatar Matej Kosik2016-06-07
| * Make Ltac Profiling an settingGravatar Jason Gross2016-06-05
| * Synchronize the profiler state with the documentGravatar Jason Gross2016-06-05
| * -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
| * Add LtacProf documentationGravatar Jason Gross2016-06-05
|/
* Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
* Fix build of documentation (broken for four months).Gravatar Guillaume Melquiond2016-06-03
* 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