Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Funind API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Quote API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Rewrite API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Eqdecide API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Hints API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Tacticals API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Clenv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Refine API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Goal API using EConstr. | 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 | |
* | | Coercion API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Tacred API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Constr_matching API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Typing API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Evarconv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Retyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Nativenorm API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | Vnorm 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 | |
| * | Adding a printer for Proof.proof reflecting the focusing layout. | Hugo Herbelin | 2017-01-26 | |
| * | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-30 | |
| |\ | ||||
| | * | Fix some documentation typos. | Guillaume Melquiond | 2016-11-24 | |
| * | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 | |
|/| | | |/ | ||||
| * | Use pf_get_type_of to avoid blowup in pose proof of large proof terms | Matthieu Sozeau | 2016-11-08 | |
| * | Merge commit 'e6edb33' into v8.6 | Maxime Dénès | 2016-11-07 | |
| |\ | ||||
| | * | More explicit name for status of unification constraints. | Maxime Dénès | 2016-11-07 | |
| * | | Fix #3441 Use pf_get_type_of to avoid blowup | Matthieu Sozeau | 2016-11-04 | |
| | * | Renamings to avoid confusion deprecating old names | Matthieu Sozeau | 2016-10-22 | |
| | * | Unification constraint handling (#4763, #5149) | Matthieu Sozeau | 2016-10-22 | |
| |/ | ||||
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-12 | |
|\| | ||||
| * | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-12 | |
| |\ | ||||
| * \ | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-12 | |
| |\ \ | ||||
| | | * | Merge remote-tracking branch 'git/bug5123' into v8.5 | Matthieu Sozeau | 2016-10-12 | |
| | |/| | ||||
| | | * | Fix bug #5123: mark all shelved evars unresolvable | Matthieu Sozeau | 2016-10-11 | |
| | * | | Fix for bug #4863, update the Proofview's env with | Matthieu Sozeau | 2016-10-11 | |
| | |/ | ||||
| | * | Fix #4416: - Incorrect "Error: Incorrect number of goals" | Arnaud Spiwack | 2016-10-10 | |
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-05 | |
|\| | |