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