Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | 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 | ||
* | | | 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 | ||
* | | | Tactic_matching API using EConstr. | 2017-02-14 | ||
* | | | Class_tactics API using EConstr. | 2017-02-14 | ||
* | | | Leminv API using EConstr. | 2017-02-14 | ||
* | | | Inv API using EConstr. | 2017-02-14 | ||
* | | | Tactics API using EConstr. | 2017-02-14 | ||
* | | | Hipattern API using EConstr. | 2017-02-14 | ||
* | | | Clenv API using EConstr. | 2017-02-14 | ||
* | | | Tacmach API using EConstr. | 2017-02-14 | ||
* | | | Refine API using EConstr. | 2017-02-14 | ||
* | | | Cleaning up opening of the EConstr module in pretyping folder. | 2017-02-14 | ||
* | | | Unification API using EConstr. | 2017-02-14 | ||
* | | | Pretyping API using EConstr. | 2017-02-14 | ||
* | | | Typeclasses API using EConstr. | 2017-02-14 | ||
* | | | Tacred API using EConstr. | 2017-02-14 | ||
* | | | Typing API using EConstr. | 2017-02-14 | ||
* | | | Evarconv API using EConstr. | 2017-02-14 | ||
* | | | Evarsolve API using EConstr. | 2017-02-14 | ||
* | | | Find_subterm API using EConstr. | 2017-02-14 | ||
* | | | Retyping API using EConstr. | 2017-02-14 | ||
* | | | Reductionops API using EConstr. | 2017-02-14 | ||
* | | | Termops API using EConstr. | 2017-02-14 | ||
| * | | Merge branch 'v8.6' | 2016-11-18 | ||
|/| | | |/ | ||||
| * | Merge remote-tracking branch 'github/pr/339' into v8.6 | 2016-11-07 | ||
| |\ | ||||
| * \ | Merge commit 'e6edb33' into v8.6 | 2016-11-07 | ||
| |\ \ | ||||
| | * | | More explicit name for status of unification constraints. | 2016-11-07 | ||
| * | | | More precise refine compatibility | 2016-11-05 | ||
| * | | | Fix #3441 Use pf_get_type_of to avoid blowup | 2016-11-04 | ||
| * | | | Fix refine in compatibility mode | 2016-11-04 | ||
* | | | | Merge branch 'v8.6' | 2016-10-29 | ||
|\| | | | ||||
| | | * | Documenting changes in typeclasses | 2016-10-29 | ||
| | |/ | |/| | ||||
| * | | Merge branch 'v8.5' into v8.6 | 2016-10-26 | ||
| |\ \ | | |/ | |/| | ||||
| | * | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | 2016-10-25 | ||
* | | | Merge branch 'v8.6' | 2016-10-08 | ||
|\| | | ||||
| * | | Fix bug #4464: "Anomaly: variable H' unbound. Please report.". | 2016-10-07 | ||
* | | | Merge branch 'v8.6' | 2016-10-05 | ||
|\| | | ||||
| * | | Merge remote-tracking branch 'github/pr/263' into v8.6 | 2016-10-03 | ||
| |\ \ | ||||
* | | | | Merge branch 'v8.6' | 2016-10-02 | ||
|\| | | | ||||
| * | | | Micro refactoring: use exact_no_check. | 2016-10-01 | ||
| * | | | Fix bug #5045: [generalize] creates ill-typed terms in 8.6. | 2016-09-30 | ||
| * | | | Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk. | 2016-09-30 | ||
* | | | | Merge branch 'v8.6' | 2016-09-27 | ||
|\| | | | ||||
| * | | | Merge branch 'v8.5' into v8.6 | 2016-09-27 | ||
| |\ \ \ | | | |/ | | |/| | ||||
| * | | | Moving "move" in the new proof engine. | 2016-09-24 | ||
| | * | | Ensuring that the evar name is preserved by "rename" as it is already | 2016-09-24 |