aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-tac.tex
AgeCommit message (Expand)Author
2016-01-20Clarifying the documentation of tactics "cbv" and "lazy".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
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-02Improving syntax of pat/constr introduction pattern so thatHugo Herbelin
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
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-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-07Document Set/Print Firstorder Solver option.Matthieu Sozeau
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
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
2014-09-10Removing "eqn:" for "induction" in reference manual.Hugo Herbelin
2014-09-08Doc: [revgoals].Arnaud Spiwack
2014-09-07Little fix in documentation of inversion.Hugo Herbelin
2014-09-03Cbn in refmanPierre Boutillier
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-07-31Typos.Hugo Herbelin
2014-07-25Document swap tactic.Arnaud Spiwack
2014-07-25Document cycle tactic.Arnaud Spiwack
2014-07-25Warns about inconsistency of generated name in evars and goals.Arnaud Spiwack
2014-05-31More on injection over a projectable "existT". - Fixing syntax "injection ......Hugo Herbelin
2014-04-04Fix for bug #3107.Guillaume Melquiond
2014-04-04fixing Function docJulien Forest
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 05:40:11 +0000