Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | 2017-05-27 | |
* | | | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | 2017-05-24 | |
| * | | Fix bug #5360: anomalies in typeclass resolution output | Matthieu Sozeau | 2017-05-16 | |
* | | | Uniformity of style for selecting plural or not; spacing for comma. | Hugo Herbelin | 2017-05-13 | |
|/ / | ||||
* | | Post-rebase warnings (unused opens and 2 unused values) | Gaetan Gilbert | 2017-04-27 | |
* | | Remove unused [open] statements | Gaetan Gilbert | 2017-04-27 | |
* | | Fix omitted labels in function calls | Gaetan Gilbert | 2017-04-27 | |
* | | Removing various tactic compatibility layers in core tactics. | Pierre-Marie Pédrot | 2017-04-24 | |
* | | Removing the tclWEAK_PROGRESS tactical. | Pierre-Marie Pédrot | 2017-04-24 | |
* | | [flags] Deprecate is_silent/is_verbose in favor of single flag. | Emilio Jesus Gallego Arias | 2017-04-21 | |
* | | Fix a heuristic used by legacy typeclass resolution. | Pierre-Marie Pédrot | 2017-04-08 | |
* | | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | 2017-04-01 | |
* | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 | |
|\ \ | ||||
| * | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-03-22 | |
| |\| | ||||
| | * | Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc... | Maxime Dénès | 2017-03-10 | |
| | |\ | ||||
* | | | | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 | |
|\| | | | ||||
* | | | | Removing a subtle nf_enter in Class_tactics. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Removing most nf_enter in tactics. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Definining EConstr-based contexts. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Removing compatibility layers related to printing. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Class_tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Hints API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Equality API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Clenv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Refine API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Goal API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Pretyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Typeclasses API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Constr_matching API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Evarconv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Retyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Termops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
| * | | | Merge remote-tracking branch 'github/pr/172' into trunk | Maxime Dénès | 2016-12-19 | |
| |\ \ \ | ||||
| * \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-12-07 | |
| |\ \ \ \ | | | |/ / | | |/| | | ||||
| | * | | | Fix shelving order in typeclasses eauto. | Théo Zimmermann | 2016-11-30 | |
| | * | | | Fix typeclasses eauto shelving. | Théo Zimmermann | 2016-11-30 | |
| * | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 | |
|/| | | | | |/ / / | ||||
| * | | | Minor debug printing bug, | Matthieu Sozeau | 2016-11-16 | |
| * | | | Revert more of a477dc for good measure | Matthieu Sozeau | 2016-11-16 |