aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
Commit message (Expand)AuthorAge
* Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Gravatar Hugo Herbelin2017-05-16
* Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
* Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\
* | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...Gravatar Hugo Herbelin2017-05-04
* | Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
* | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | Add [_] prefix to unused values which maybe should be keptGravatar Gaetan Gilbert2017-04-27
* | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
* | Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
|/
* Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
* \ Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \
| * | [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | | Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ | |/ / |/| |
| * | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \
* | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| |
* | | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \
| | * | Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
| | * | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| | |\ \ | |_|/ / |/| | |
* | | | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \ \ \
| | | * | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | | | | Declaring ltac plugin, so that static linking works.Gravatar Hugo Herbelin2017-04-01
| | | * | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | * | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| |_|/ / |/| | |
| * | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
|/ / /
| * | Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| * | Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
|/ /
* | [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [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
| | * [ltac] Move dummy plugin to plugins folder.Gravatar Emilio Jesus Gallego Arias2017-03-03
* | 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-06-20 12:25:13 +0000