Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Remove unused [open] statements | 2017-04-27 | |
* | Merge branch 'master' into econstr | 2017-04-07 | |
|\ | |||
* | | Removing a normalization hotspot from EConstr. | 2017-04-05 | |
* | | Using delayed universe instances in EConstr. | 2017-04-01 | |
* | | Actually exporting delayed universes in the EConstr implementation. | 2017-04-01 | |
* | | Merge branch 'trunk' into pr379 | 2017-03-24 | |
|\ \ | |||
| | * | Better algorithm for Evarconv.max_undefined_with_candidates. | 2017-03-24 | |
| |/ | |||
* | | Merge branch 'master'. | 2017-02-14 | |
|\ \ | |||
* | | | Chasing a few unsafe constr coercions. | 2017-02-14 | |
* | | | Definining EConstr-based contexts. | 2017-02-14 | |
* | | | Evar-normalizing functions now act on EConstrs. | 2017-02-14 | |
* | | | Removing compatibility layers related to printing. | 2017-02-14 | |
* | | | Removing compatibility layers in Retyping | 2017-02-14 | |
* | | | Removing some return type compatibility layers in Termops. | 2017-02-14 | |
* | | | Eliminating parts of the right-hand side compatibility layer | 2017-02-14 | |
* | | | Tactics API using EConstr. | 2017-02-14 | |
* | | | Clenv API using EConstr. | 2017-02-14 | |
* | | | Cleaning up opening of the EConstr module in pretyping folder. | 2017-02-14 | |
* | | | Making judgment type generic over the type of inner constrs. | 2017-02-14 | |
* | | | Unification API using EConstr. | 2017-02-14 | |
* | | | Pretyping API using EConstr. | 2017-02-14 | |
* | | | Tacred API using EConstr. | 2017-02-14 | |
* | | | Evarconv API using EConstr. | 2017-02-14 | |
* | | | Evarsolve API using EConstr. | 2017-02-14 | |
* | | | Evardefine 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 | |
| | * | Improve unification debug trace. | 2016-12-13 | |
| |/ | |||
| * | Merge branch 'v8.6' | 2016-11-18 | |
|/| | |||
| * | Merge commit 'e6edb33' into v8.6 | 2016-11-07 | |
| |\ | |||
* | | | Stronger static invariant in equality upto universes. | 2016-10-31 | |
* | | | Merge branch 'v8.6' | 2016-10-29 | |
|\| | | |||
| * | | Merge branch 'v8.5' into v8.6 | 2016-10-26 | |
| |\ \ | |||
| | | * | Renamings to avoid confusion deprecating old names | 2016-10-22 | |
| | |/ | |/| | |||
| | * | Fix a bug in error printing of unif constraints | 2016-10-22 | |
* | | | Merge branch 'v8.6' | 2016-10-18 | |
|\| | | |||
| * | | Merge branch 'v8.5' into v8.6 | 2016-10-18 | |
| |\| | |||
| * | | Quick fix to unification regression #4955. | 2016-10-17 | |
| | * | Fixing a missing constraint in consider_remaining_unif_constraints. | 2016-10-17 | |
* | | | Merge branch 'v8.6' | 2016-10-08 | |
|\| | | |||
| * | | Merge branch 'v8.5' into v8.6 | 2016-10-08 | |
| |\| | |||
| | * | evarconv.ml: Fix bug #4529, primproj unfolding | 2016-10-06 | |
* | | | Merge branch 'v8.6' | 2016-09-14 | |
|\| | | |||
| * | | no-refold patch | 2016-09-09 | |
* | | | Merge PR #244. | 2016-09-08 | |
|\ \ \ | |||
* | | | | CLEANUP: using |> operator more consistently | 2016-08-30 | |
* | | | | CLEANUP: minor readability improvements | 2016-08-24 | |
* | | | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function | 2016-08-24 | |
| |/ / |/| | | |||
| * | | Unify location handling of error functions. | 2016-08-19 | |
|/ / |