Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Rewrite API using EConstr. | 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 | ||
* | | Coercion 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 | ||
* | | Evardefine 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 | ||
|/| | ||||
* | | Stronger static invariant in equality upto universes. | 2016-10-31 | ||
* | | Merge branch 'v8.6' | 2016-10-24 | ||
|\ \ | ||||
| | * | Renamings to avoid confusion deprecating old names | 2016-10-22 | ||
| | * | Unification constraint handling (#4763, #5149) | 2016-10-22 | ||
| | * | Port fix for bugs 4763, 5149, previously 0b417c12e | 2016-10-22 | ||
| |/ | ||||
| * | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | 2016-10-21 | ||
| |\ | ||||
| | * | Revert "unification.ml: fix for bug #4763, unif regression" | 2016-10-21 | ||
* | | | Merge branch 'v8.6' | 2016-10-08 | ||
|\| | | ||||
| * | | Merge branch 'v8.5' into v8.6 | 2016-10-08 | ||
| |\| | ||||
| | * | w_merge: Add a comment about the (List.rev evars) | 2016-10-06 | ||
| | * | unification.ml: fix for bug #4763, unif regression | 2016-10-06 | ||
* | | | 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-09-23 | ||
|\| | | | ||||
| * | | | Merge branch 'v8.5' into v8.6 | 2016-09-23 | ||
| |\ \ \ | | | |/ | | |/| | ||||
| | * | | Fixing #5095 (non relevant too strict test in let-in abstraction). | 2016-09-22 | ||
* | | | | Merge branch 'v8.6' | 2016-09-14 | ||
|\| | | | ||||
| * | | | no-refold patch | 2016-09-09 | ||
| | | * | Tracking careless uses of slow name lookup. | 2016-09-09 | ||
| | |/ | |/| | ||||
* | | | Merge PR #244. | 2016-09-08 | ||
|\ \ \ | ||||
* \ \ \ | Merge remote-tracking branch 'v8.6' into trunk | 2016-08-25 | ||
|\ \ \ \ | | |/ / | |/| | | ||||
* | | | | CLEANUP: minor readability improvements | 2016-08-24 | ||
| * | | | Pushing error backtrace in unification reraise. | 2016-08-22 | ||
|/ / / | ||||
| * | | Make the user_err header an optional parameter. | 2016-08-19 | ||
| * | | Remove errorlabstrm in favor of user_err | 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 | ||
* | | Separate flags for fix/cofix/match reduction and clean reduction function names. | 2016-07-01 | ||
* | | A mini-optimization for free in unification.ml: test in O(1) | 2016-06-10 | ||
* | | Feedback cleanup | 2016-05-31 | ||
* | | Splitting Evarutil in two distinct files. | 2016-03-20 | ||
* | | Merge branch 'v8.5' | 2016-03-20 | ||
|\| |