aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2016-06-20Reference Manual / Extraction: the original example command no longer works w...Matej Kosik
2016-06-19Add [Unset Printing Dependent Evars Line]Jason Gross
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-16Document new Hint Mode option.Matthieu Sozeau
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-15typographyMatej Kosik
2016-06-14Add documentation for goal selectors.Cyprien Mangin
2016-06-14-async-proofs-delegation-threshold default value set to 0.03Enrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-14Merge branch "LtacProf for trunk" (PR #165).Pierre-Marie Pédrot
2016-06-13Univs: more robust Universe/Constraint decls #4816Matthieu Sozeau
2016-06-07typoMatej Kosik
2016-06-07typographyMatej Kosik
2016-06-07DocumentationEnrico Tassi
2016-06-05Make Ltac Profiling an settingJason Gross
2016-06-05Synchronize the profiler state with the documentJason Gross
2016-06-05-profileltac -> -profile-ltac, as per @herbelinJason Gross
2016-06-05Add LtacProf documentationJason Gross
2016-06-05Adding the Print Ltac Signature command.Pierre-Marie Pédrot
2016-05-15Fix a really small doc typoRicky Elrod
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 11:18:28 +0000