aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ltac.tex
Commit message (Expand)AuthorAge
* Documenting the existence of first and solve as Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
* Add documentation for Set Ltac Batch DebugGravatar Jason Gross2017-05-11
* Mark transparent_abstract as risky in docsGravatar Jason Gross2017-04-25
* Add transparent_abstract tacticGravatar Jason Gross2017-04-25
* Merge remote-tracking branch 'github/pr/280' into v8.6Gravatar Maxime Dénès2016-09-30
|\
* \ Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
|\ \
| | * Doc: [Reset Ltac Profile] is not synchronizedGravatar Jason Gross2016-09-16
| |/ |/|
* | Fix a typo in the reference manualGravatar Jason Gross2016-09-07
* | In docs, fix command to reset Ltac profilingGravatar Paul Steckler2016-08-17
| * Update the documentation for goal selectors.Gravatar Cyprien Mangin2016-06-30
|/
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* Add documentation for goal selectors.Gravatar Cyprien Mangin2016-06-14
* Make Ltac Profiling an settingGravatar Jason Gross2016-06-05
* Synchronize the profiler state with the documentGravatar Jason Gross2016-06-05
* -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
* Add LtacProf documentationGravatar Jason Gross2016-06-05
* Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
* TYPOGRAPHY: correction of one particular error in the Reference ManualGravatar Matej Kosik2015-12-18
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\
| * Reference Manual: Applying standard style recommendation about notGravatar Hugo Herbelin2015-10-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-12
|\|
| * Documenting matching under binders.Gravatar Hugo Herbelin2015-10-11
* | Documenting the Shrink Abstract option.Gravatar Pierre-Marie Pédrot2015-08-22
|/
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* Fixed doc of fresh (was already outdated before fixing #3233).Gravatar Pierre Courtieu2015-02-23
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Fix index of reference manual.Gravatar Guillaume Melquiond2015-01-29
* Reference manual: fix typo in doc of [tryif/then/else].Gravatar Arnaud Spiwack2015-01-21
* Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Gravatar Arnaud Spiwack2015-01-14
* Reference manual: document tryif/then/else.Gravatar Arnaud Spiwack2015-01-14
* Reference manual: document multimatch.Gravatar Arnaud Spiwack2015-01-14
* Reference manual: try and improve documentation for Ltac's match.Gravatar Arnaud Spiwack2015-01-14
* Reference manual: try and improve the documentation of lazymatch.Gravatar Arnaud Spiwack2015-01-14
* Reference manual: document gfail.Gravatar Arnaud Spiwack2015-01-14
* Document the new behavior of lazymatch.Gravatar Guillaume Melquiond2014-12-30
* Document [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Fix typo in documentation of the [repeat] tactical.Gravatar Arnaud Spiwack2014-10-24
* Removing remaining documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-11
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Documentation: a simple example for [numgoals].Gravatar Arnaud Spiwack2014-08-05
* Documentation of [uconstr]: typesetting.Gravatar Arnaud Spiwack2014-08-05
* Documentation: refine accept uconstr arguments.Gravatar Arnaud Spiwack2014-08-05
* Document [> … ].Gravatar Arnaud Spiwack2014-08-01
* Fix English spelling -> American spelling in doc.Gravatar Arnaud Spiwack2014-08-01
* Document [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Document untyped terms in tactics.Gravatar Arnaud Spiwack2014-07-29
* Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...Gravatar Arnaud Spiwack2014-07-25
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13