aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ltac.tex
AgeCommit message (Expand)Author
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
2015-12-18TYPOGRAPHY: correction of one particular error in the Reference ManualMatej Kosik
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-18Reference Manual: Applying standard style recommendation about notHugo Herbelin
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-11Documenting matching under binders.Hugo Herbelin
2015-08-22Documenting the Shrink Abstract option.Pierre-Marie Pédrot
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-02-23Fixed doc of fresh (was already outdated before fixing #3233).Pierre Courtieu
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-01-29Fix index of reference manual.Guillaume Melquiond
2015-01-21Reference manual: fix typo in doc of [tryif/then/else].Arnaud Spiwack
2015-01-14Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Arnaud Spiwack
2015-01-14Reference manual: document tryif/then/else.Arnaud Spiwack
2015-01-14Reference manual: document multimatch.Arnaud Spiwack
2015-01-14Reference manual: try and improve documentation for Ltac's match.Arnaud Spiwack
2015-01-14Reference manual: try and improve the documentation of lazymatch.Arnaud Spiwack
2015-01-14Reference manual: document gfail.Arnaud Spiwack
2014-12-30Document the new behavior of lazymatch.Guillaume Melquiond
2014-11-01Document [Info] command.Arnaud Spiwack
2014-10-24Fix typo in documentation of the [repeat] tactical.Arnaud Spiwack
2014-09-11Removing remaining documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-03sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texPierre Boutillier
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-05Documentation: a simple example for [numgoals].Arnaud Spiwack
2014-08-05Documentation of [uconstr]: typesetting.Arnaud Spiwack
2014-08-05Documentation: refine accept uconstr arguments.Arnaud Spiwack
2014-08-01Document [> … ].Arnaud Spiwack
2014-08-01Fix English spelling -> American spelling in doc.Arnaud Spiwack
2014-08-01Document [numgoals] and [guard].Arnaud Spiwack
2014-07-29Document untyped terms in tactics.Arnaud Spiwack
2014-07-25Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...Arnaud Spiwack
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-04-02Fix Bug 3131 + Really drop mentions of info in refman.Pierre Boutillier
2014-01-01Reference the 'external' tactic.Guillaume Melquiond
2013-12-03Silence some warning about references in documentation.Guillaume Melquiond
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
2013-11-02Documentation for the backtracking features.aspiwack
2013-08-08Manual fixed w.r.t. STMgareuselesinge
2013-05-29Documenting the "appcontext" by default.ppedrot
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-01-20Added documentation for "r foo" in Ltac debugger.herbelin
2011-11-29Documentation of appcontextletouzey
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2010-10-05(Hopefully) clearer explanation of Ltac's context patternsglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 20:56:12 +0000