aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ltac.tex
AgeCommit message (Expand)Author
2018-04-14[Sphinx] Move chapter 9 to new infrastructure.Théo Zimmermann
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
2018-02-28Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Hugo Herbelin
2018-01-03add optimize_heap tactic for #6488Paul Steckler
2017-12-19Fix typo in the refman.Théo Zimmermann
2017-12-14Add documentation for time_constrJason Gross
2017-12-14Add doc+changelog entries for new LtacProf tacticsJason Gross
2017-12-11Remove deprecated appcontext and corresponding documentation.Théo Zimmermann
2017-12-01clarify operation of sequences, #6095Paul Steckler
2017-11-06Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Samuel Gruetter
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-07-11Sync the manual with the deprecation warnings.Théo Zimmermann
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-26Merge PR#756: Fix Bug #5574, document function scopeMaxime Dénès
2017-06-23Fix Bug #5574, document function scopePaul Steckler
2017-06-13Document evar naming syntax.Théo Zimmermann
2017-05-27Documenting the existence of first and solve as Ltac definitions.Pierre-Marie Pédrot
2017-05-11Add documentation for Set Ltac Batch DebugJason Gross
2017-04-25Mark transparent_abstract as risky in docsJason Gross
2017-04-25Add transparent_abstract tacticJason Gross
2016-09-30Merge remote-tracking branch 'github/pr/280' into v8.6Maxime Dénès
2016-09-28Merge remote-tracking branch 'github/pr/232' into v8.6Maxime Dénès
2016-09-16Doc: [Reset Ltac Profile] is not synchronizedJason Gross
2016-09-07Fix a typo in the reference manualJason Gross
2016-08-17In docs, fix command to reset Ltac profilingPaul Steckler
2016-06-30Update the documentation for goal selectors.Cyprien Mangin
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-14Add documentation for goal selectors.Cyprien Mangin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 01:33:47 +0000