Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Removing various compatibility layers of tactics. | 2017-02-14 | ||
* | | Funind API using EConstr. | 2017-02-14 | ||
* | | Ltac now uses evar-based constrs. | 2017-02-14 | ||
* | | Removing compatibility layers in Retyping | 2017-02-14 | ||
* | | Quote API using EConstr. | 2017-02-14 | ||
* | | Reductionops now return EConstrs. | 2017-02-14 | ||
* | | 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 | ||
|\| | | |