Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | | funind: Ignore missing info for current function | 2017-03-22 | ||
| |/ / / | ||||
* | | | | [extraction] Flush formatters at end of output. | 2017-03-21 | ||
* | | | | [pp] Move terminal-specific tagging to the toplevel. | 2017-03-21 | ||
* | | | | [pp] Make feedback the only logging mechanism. | 2017-03-21 | ||
* | | | | [pp] Force well-formed boxes by construction. | 2017-03-21 | ||
* | | | | [pp] Prepare for serialization, remove opaque glue. | 2017-03-21 | ||
* | | | | [pp] Remove `Pp.stras`. | 2017-03-21 | ||
* | | | | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list` | 2017-03-21 | ||
* | | | | [pp] Remove unused printing tagging infrastructure. | 2017-03-21 | ||
* | | | | Merge PR#134: Enable `-safe-string` | 2017-03-21 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR#428: Report missing tactic arguments in error message | 2017-03-17 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR#445: TACTIC EXTEND now takes an optional level as argument. | 2017-03-17 | ||
|\ \ \ \ \ \ | ||||
* | | | | | | | Attempt to improve error message when "apply in" fail. | 2017-03-15 | ||
| | | * | | | | [safe-string] plugins/extraction | 2017-03-14 | ||
| | | * | | | | [safe-string] ltac/profile_ltac | 2017-03-14 | ||
| |_|/ / / / |/| | | | | | ||||
| | * | | | | Report missing tactic arguments in error message | 2017-03-14 | ||
| |/ / / / |/| | | | | ||||
* | | | | | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun | 2017-03-14 | ||
|\ \ \ \ \ | ||||
* | | | | | | Micromega: removing a constant preventing micromega to be loaded before Logic.v. | 2017-03-09 | ||
| | | | * | | Farewell decl_mode | 2017-03-07 | ||
| |_|_|/ / |/| | | | | ||||
| | | * | | [ltac] Move dummy plugin to plugins folder. | 2017-03-03 | ||
* | | | | | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or | 2017-02-27 | ||
|\ \ \ \ \ | ||||
| | | * | | | TACTIC EXTEND now takes an optional level as argument. | 2017-02-24 | ||
| |_|/ / / |/| | | | | ||||
* | | | | | Revert "Add empty ltac_plugin file for forward compatibility." | 2017-02-24 | ||
* | | | | | Merge branch 'v8.6' | 2017-02-22 | ||
|\ \ \ \ \ | | |_|/ / | |/| | | | ||||
* | | | | | Moving the Ltac plugin to a pack-based one. | 2017-02-17 | ||
* | | | | | Ltac as a plugin. | 2017-02-17 | ||
| | | * | | [cleanup] Change Id.t option to Name.t in TacFun | 2017-02-16 | ||
| |_|/ / |/| | | | ||||
| | | * | Merge branch 'master'. | 2017-02-14 | ||
| | | |\ | |_|_|/ |/| | | | ||||
| | | * | Porting the ssrmatching plugin to the new EConstr API. | 2017-02-14 | ||
| | | * | Quick hack to fix interpretation of patterns in Ltac. | 2017-02-14 | ||
| | | * | Removing most nf_enter in tactics. | 2017-02-14 | ||
| | | * | Fix a mishandled exception in Omega. | 2017-02-14 | ||
| | | * | Namegen primitives now apply on evar constrs. | 2017-02-14 | ||
| | | * | Definining EConstr-based contexts. | 2017-02-14 | ||
| | | * | Evar-normalizing functions now act on EConstrs. | 2017-02-14 | ||
| | | * | Removing compatibility layers from Tacticals | 2017-02-14 | ||
| | | * | Omega API using EConstr. | 2017-02-14 | ||
| | | * | Micromega API using EConstr. | 2017-02-14 | ||
| | | * | Removing various compatibility layers of tactics. | 2017-02-14 | ||
| | | * | Funind API using EConstr. | 2017-02-14 | ||
| | | * | Removing compatibility layers related to printing. | 2017-02-14 | ||
| | | * | Ltac now uses evar-based constrs. | 2017-02-14 | ||
| | | * | Removing compatibility layers in Retyping | 2017-02-14 | ||
| | | * | Removing some return type compatibility layers in Termops. | 2017-02-14 | ||
| | | * | Setoid_ring API using EConstr. | 2017-02-14 | ||
| | | * | Cc API using EConstr. | 2017-02-14 | ||
| | | * | Quote API using EConstr. | 2017-02-14 | ||
| | | * | Reductionops now return EConstrs. | 2017-02-14 | ||
| | | * | Proofview.Goal primitive now return EConstrs. | 2017-02-14 | ||
| | | * | Eliminating parts of the right-hand side compatibility layer | 2017-02-14 |