Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | 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 | ||
|/ / | ||||
* | | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) | 2016-07-03 | ||
* | | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | 2016-07-03 | ||
* | | Univs: add source locations of levels | 2016-06-29 | ||
* | | Refine 9cc95f5, unification of Let-In's, bug #3929 | 2016-06-16 | ||
* | | Merge branch 'v8.5' | 2016-06-13 | ||
|\| | ||||
| * | evar_conv: Refine occur_rigidly | 2016-06-13 | ||
| * | Minor simplification in evarconv. | 2016-06-12 | ||
| * | Protecting eta-expansion in evarconv.ml against ill-typed problems. | 2016-06-12 | ||
* | | Merge branch 'v8.5' | 2016-06-09 | ||
|\| | ||||
| * | Fixing #4644 (regression of unification on evar-evar problems with a match). | 2016-06-09 | ||
| * | Minor simplification in evarconv.ml. | 2016-06-09 | ||
* | | Feedback cleanup | 2016-05-31 | ||
* | | Splitting Evarutil in two distinct files. | 2016-03-20 | ||
* | | Merge branch 'v8.5' | 2016-03-20 | ||
|\| | ||||
* | | Merge branch 'v8.5' | 2016-03-18 | ||
|\ \ | ||||
| | * | Fix incorrect behavior of CS resolution | 2016-03-16 | ||
| |/ |