aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
...
| | | * | | | [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
|\ \ \ \ \
* | | | | | Micromega: removing a constant preventing micromega to be loaded before Logic.v.Gravatar Hugo Herbelin2017-03-09
| | | | * | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|_|/ / |/| | | |
| | | * | [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
| | | * | [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
| |_|/ / |/| | |
| | | * Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |\ | |_|_|/ |/| | |
| | | * Porting the ssrmatching plugin to the new EConstr API.Gravatar Enrico Tassi2017-02-14
| | | * Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Fix a mishandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
| | | * Omega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Micromega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
| | | * Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Setoid_ring API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
| | | * Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 10:08:04 +0000