Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | Proofview.Goal primitive now return EConstrs. | 2017-02-14 | ||
* | | | Eliminating parts of the right-hand side compatibility layer | 2017-02-14 | ||
* | | | Rewrite API using EConstr. | 2017-02-14 | ||
* | | | Eqdecide API using EConstr. | 2017-02-14 | ||
* | | | Hints API using EConstr. | 2017-02-14 | ||
* | | | Tactics API using EConstr. | 2017-02-14 | ||
* | | | Tacticals 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 | ||
* | | | Goal API using EConstr. | 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 | ||
* | | | Constr_matching API using EConstr. | 2017-02-14 | ||
* | | | Typing API using EConstr. | 2017-02-14 | ||
* | | | Evarconv API using EConstr. | 2017-02-14 | ||
* | | | Retyping API using EConstr. | 2017-02-14 | ||
* | | | Nativenorm API using EConstr. | 2017-02-14 | ||
* | | | Vnorm API using EConstr. | 2017-02-14 | ||
* | | | Reductionops API using EConstr. | 2017-02-14 | ||
* | | | Termops API using EConstr. | 2017-02-14 | ||
| * | | Adding a printer for Proof.proof reflecting the focusing layout. | 2017-01-26 | ||
| * | | Merge branch 'v8.6' | 2016-11-30 | ||
| |\| | ||||
| | * | Fix some documentation typos. | 2016-11-24 | ||
| * | | Merge branch 'v8.6' | 2016-11-18 | ||
|/| | | |/ | ||||
| * | Use pf_get_type_of to avoid blowup in pose proof of large proof terms | 2016-11-08 | ||
| * | Merge commit 'e6edb33' into v8.6 | 2016-11-07 | ||
| |\ | ||||
| | * | More explicit name for status of unification constraints. | 2016-11-07 | ||
| * | | Fix #3441 Use pf_get_type_of to avoid blowup | 2016-11-04 | ||
| | * | Renamings to avoid confusion deprecating old names | 2016-10-22 | ||
| | * | Unification constraint handling (#4763, #5149) | 2016-10-22 | ||
| |/ | ||||
* | | Merge branch 'v8.6' | 2016-10-12 | ||
|\| | ||||
| * | Merge branch 'v8.5' into v8.6 | 2016-10-12 | ||
| |\ | ||||
| * \ | Merge branch 'v8.5' into v8.6 | 2016-10-12 | ||
| |\ \ | ||||
| | | * | Merge remote-tracking branch 'git/bug5123' into v8.5 | 2016-10-12 | ||
| | |/| | ||||
| | | * | Fix bug #5123: mark all shelved evars unresolvable | 2016-10-11 | ||
| | * | | Fix for bug #4863, update the Proofview's env with | 2016-10-11 | ||
| | |/ | ||||
| | * | Fix #4416: - Incorrect "Error: Incorrect number of goals" | 2016-10-10 | ||
* | | | 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 | ||
|\| | | | ||||
| * | | | Fix bug #4723 and FIXME in API for solve_by_tac | 2016-09-28 | ||
* | | | | Merge branch 'v8.6' | 2016-09-27 | ||
|\| | | | ||||
| * | | | Moving "move" in the new proof engine. | 2016-09-24 | ||
* | | | | Merge branch 'v8.6' | 2016-09-23 | ||
|\| | | | ||||
* | | | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk" | 2016-09-22 | ||
* | | | | Stylistic improvements in intf/decl_kinds.mli. | 2016-09-20 |