aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-tac.tex
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-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-20Clarifying the documentation of tactics "cbv" and "lazy".Hugo Herbelin
2016-01-14Updating and improving the documentation of intros patterns.Hugo Herbelin
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
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
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Simplifying documentation of "assert form as pat".Hugo Herbelin
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Improving syntax of pat/constr introduction pattern so thatHugo Herbelin
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Fixing error messages about Hint.Hugo Herbelin
2015-10-02Improving reference manual in that auto uses simple apply rather than apply.Hugo Herbelin
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-02Granting Jason's request for an ad hoc compatibility option onHugo Herbelin
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-07Document Set/Print Firstorder Solver option.Matthieu Sozeau
2015-05-15Turning "Set Regular Subst Tactic" on by default (for 8.6).Hugo Herbelin
2015-05-13Documenting Set Regular Subst Tactic (though unsure this is worth theHugo Herbelin
2015-05-13Documenting the Loose Hint Behavior flag.Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-05Preprend Fail to all the expected failures in the documentation.Guillaume Melquiond
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-17Remove non-existing Tactic Definition command from index.Maxime Dénès
2015-02-16Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.Hugo Herbelin
2015-02-10Fix documentation of generalize. (Fix for bug #4015)Guillaume Melquiond
2015-02-10Fix some documentation typo.Guillaume Melquiond
2015-01-29Fix some broken Coq scripts in the reference manual.Guillaume Melquiond
2015-01-24Reference Manual: Documenting new printing of evars and new effect ofHugo Herbelin
2015-01-08Document native_compute.Maxime Dénès
2014-12-09refman: avoid label names with whitespace (unsupported in html)Pierre Letouzey
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-07Fixing doc of Functional Induction.Hugo Herbelin
2014-11-04Documenting the change of semantics of the replace tactic.Pierre-Marie Pédrot
2014-10-24Addressing report #3279 (inconsistency of behavior of the -> and <-Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:35:02 +0000