aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/profile_ltac.ml
Commit message (Expand)AuthorAge
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [safe-string] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17