aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
2017-04-07[camlpX] Remove camlp4 compat layer.Emilio Jesus Gallego Arias
2017-04-06Merge PR#508: Optimize pending evarsMaxime Dénès
2017-04-03Merge PR#417: No cast surgery in let inMaxime Dénès
2017-04-01Declaring ltac plugin, so that static linking works.Hugo Herbelin
2017-03-24Unifying standard "constr_level" names for constructors of local_binder_expr.Hugo Herbelin
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2017-03-23Fast path for implicit tactic solving.Pierre-Marie Pédrot
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-03-21[pp] Move terminal-specific tagging to the toplevel.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
2017-03-21Merge PR#134: Enable `-safe-string`Maxime Dénès
2017-03-17Merge PR#428: Report missing tactic arguments in error messageMaxime Dénès
2017-03-17Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Maxime Dénès
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
2017-03-14[safe-string] ltac/profile_ltacEmilio Jesus Gallego Arias
2017-03-14Report missing tactic arguments in error messageTej Chajed
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-02-27Merge PR#395: Allow hintdb to be parameters in a Ltac definition orMaxime Dénès
2017-02-24TACTIC EXTEND now takes an optional level as argument.Maxime Dénès
2017-02-24Revert "Add empty ltac_plugin file for forward compatibility."Maxime Dénès
2017-02-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 01:09:18 +0000