aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
Commit message (Expand)AuthorAge
* [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
|\
* \ Merge PR#428: Report missing tactic arguments in error messageGravatar Maxime Dénès2017-03-17
|\ \
* \ \ Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-03-17
|\ \ \
* | | | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| | | * [safe-string] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
| |_|/ |/| |
| | * Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
| |/ |/|
* | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
* | Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
| * TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
|/
* Revert "Add empty ltac_plugin file for forward compatibility."Gravatar Maxime Dénès2017-02-24
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
* Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 03:07:55 +0000