Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | Merge branch 'master' into econstr | 2017-04-07 | ||
| |\ \ \ \ | ||||
* | | | | | | [camlpX] Remove camlp4 compat layer. | 2017-04-07 | ||
| |/ / / / |/| | | | | ||||
* | | | | | Merge PR#455: Farewell decl_mode | 2017-04-06 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR#508: Optimize pending evars | 2017-04-06 | ||
|\ \ \ \ \ \ | ||||
| | | * | | | | Fix a normalization hotspot in computation of constr keys. | 2017-04-06 | ||
| | | | | | * | end of correction of bug 4306 | 2017-04-04 | ||
| | | | | | * | Bad correction in previous commit | 2017-04-04 | ||
| | | | | | * | Solving first problem in bug #4306. TO DO : solve the let in problem | 2017-04-04 | ||
| | | | | |/ | ||||
| | | * | | | Merge branch 'trunk' into pr379 | 2017-04-04 | ||
| | | |\ \ \ | |_|_|/ / / |/| | | | | | ||||
* | | | | | | Merge PR#417: No cast surgery in let in | 2017-04-03 | ||
|\ \ \ \ \ \ | ||||
| | | | * | | | Using delayed universe instances in EConstr. | 2017-04-01 | ||
* | | | | | | | Declaring ltac plugin, so that static linking works. | 2017-04-01 | ||
| | | | * | | | Actually exporting delayed universes in the EConstr implementation. | 2017-04-01 | ||
| | | | * | | | Merge branch 'trunk' into pr379 | 2017-03-24 | ||
| | | | |\ \ \ | |_|_|_|/ / / |/| | | | | | | ||||
| * | | | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | 2017-03-24 | ||
| * | | | | | | Unifying standard "constr_level" names for constructors of local_binder_expr. | 2017-03-24 | ||
| * | | | | | | Renaming local_binder into local_binder_expr. | 2017-03-24 | ||
| * | | | | | | "Standardizing" the name LocalPatten into LocalRawPattern. | 2017-03-24 | ||
|/ / / / / / | ||||
| | | | * / | Improving the API of constrexpr_ops.mli. | 2017-03-23 | ||
| |_|_|/ / |/| | | | | ||||
* | | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220." | 2017-03-23 | ||
* | | | | | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
|\ \ \ \ \ | | |_|_|/ | |/| | | | ||||
| * | | | | Merge PR#495: funind: Ignore missing info for current function | 2017-03-23 | ||
| |\ \ \ \ | ||||
| | | * | | | Fast path for implicit tactic solving. | 2017-03-23 | ||
| | | * | | | Ensuring static invariants about handling of pending evars in Pretyping. | 2017-03-23 | ||
| * | | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220. | 2017-03-23 | ||
* | | | | | | Mark ring morphisms as opaque. | 2017-03-22 | ||
* | | | | | | Change the parser and printer so that they use IZR for real constants. | 2017-03-22 | ||
* | | | | | | Fix broken evaluation strategies for ring and field. | 2017-03-22 | ||
* | | | | | | Remove duplicate lemmas. | 2017-03-22 | ||
| |_|/ / / |/| | | | | ||||
| | * | | | 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 | ||
|\ \ \ \ \ |