| Age | Commit message (Expand) | Author |
|---|
| 2017-12-01 | clarify operation of sequences, #6095 | Paul Steckler |
| 2017-11-06 | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | Samuel Gruetter |
| 2017-09-29 | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond |
| 2017-07-11 | Sync the manual with the deprecation warnings. | Théo Zimmermann |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-06-26 | Merge PR#756: Fix Bug #5574, document function scope | Maxime Dénès |
| 2017-06-23 | Fix Bug #5574, document function scope | Paul Steckler |
| 2017-06-13 | Document evar naming syntax. | Théo Zimmermann |
| 2017-05-27 | Documenting the existence of first and solve as Ltac definitions. | Pierre-Marie Pédrot |
| 2017-05-11 | Add documentation for Set Ltac Batch Debug | Jason Gross |
| 2017-04-25 | Mark transparent_abstract as risky in docs | Jason Gross |
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross |
| 2016-09-30 | Merge remote-tracking branch 'github/pr/280' into v8.6 | Maxime Dénès |
| 2016-09-28 | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès |
| 2016-09-16 | Doc: [Reset Ltac Profile] is not synchronized | Jason Gross |
| 2016-09-07 | Fix a typo in the reference manual | Jason Gross |
| 2016-08-17 | In docs, fix command to reset Ltac profiling | Paul Steckler |
| 2016-06-30 | Update the documentation for goal selectors. | Cyprien Mangin |
| 2016-06-17 | par: like all: but in parallel | Enrico Tassi |
| 2016-06-14 | Add documentation for goal selectors. | Cyprien Mangin |
| 2016-06-05 | Make Ltac Profiling an setting | Jason Gross |
| 2016-06-05 | Synchronize the profiler state with the document | Jason Gross |
| 2016-06-05 | -profileltac -> -profile-ltac, as per @herbelin | Jason Gross |
| 2016-06-05 | Add LtacProf documentation | Jason Gross |
| 2016-06-05 | Adding the Print Ltac Signature command. | Pierre-Marie Pédrot |
| 2015-12-18 | TYPOGRAPHY: correction of one particular error in the Reference Manual | Matej Kosik |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-18 | Reference Manual: Applying standard style recommendation about not | Hugo Herbelin |
| 2015-10-12 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-11 | Documenting matching under binders. | Hugo Herbelin |
| 2015-08-22 | Documenting the Shrink Abstract option. | Pierre-Marie Pédrot |
| 2015-03-22 | Qed export -> Qed exporting | Enrico Tassi |
| 2015-02-23 | Fixed doc of fresh (was already outdated before fixing #3233). | Pierre Courtieu |
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi |
| 2015-01-29 | Fix index of reference manual. | Guillaume Melquiond |
| 2015-01-21 | Reference manual: fix typo in doc of [tryif/then/else]. | Arnaud Spiwack |
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack |
| 2015-01-14 | Reference manual: try and improve documentation for Ltac's match. | Arnaud Spiwack |
| 2015-01-14 | Reference manual: try and improve the documentation of lazymatch. | Arnaud Spiwack |
| 2015-01-14 | Reference manual: document gfail. | Arnaud Spiwack |
| 2014-12-30 | Document the new behavior of lazymatch. | Guillaume Melquiond |
| 2014-11-01 | Document [Info] command. | Arnaud Spiwack |
| 2014-10-24 | Fix typo in documentation of the [repeat] tactical. | Arnaud Spiwack |
| 2014-09-11 | Removing remaining documentation of the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-03 | sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex | Pierre Boutillier |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
