Commit message (Expand) | Author | Age | |
---|---|---|---|
* | 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 |
* | 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 |
|\| | | |||
| * | | Merge remote-tracking branch 'github/pr/263' into v8.6 | Maxime Dénès | 2016-10-03 |
| |\ \ | |||
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-02 |
|\| | | | |||
| * | | | Fix bug #4723 and FIXME in API for solve_by_tac | Matthieu Sozeau | 2016-09-28 |
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-27 |
|\| | | | |||
| * | | | Moving "move" in the new proof engine. | Hugo Herbelin | 2016-09-24 |
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-23 |
|\| | | | |||
* | | | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk" | Maxime Dénès | 2016-09-22 |
* | | | | Stylistic improvements in intf/decl_kinds.mli. | Maxime Dénès | 2016-09-20 |
| * | | | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin | 2016-09-16 |
* | | | | Make the Coq codebase independent from Ltac-related code. | Pierre-Marie Pédrot | 2016-09-16 |
|\ \ \ \ | |||
* \ \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-14 |
|\ \ \ \ \ | | |/ / / | |/| | | | |||
| * | | | | Merge remote-tracking branch 'github-coq/pr/249' into v8.6 | Matthieu Sozeau | 2016-09-12 |
| |\ \ \ \ | |||
| | * | | | | no-refold patch | Paul Steckler | 2016-09-09 |
| * | | | | | Fast path in Clenvtac.clenv_refine typeclass resolution. | Pierre-Marie Pédrot | 2016-09-09 |
| |/ / / / | |||
| | | * / | Tracking careless uses of slow name lookup. | Pierre-Marie Pédrot | 2016-09-09 |
| | |/ / | |/| | | |||
| | * | | Making Proof_global terminator generic in external tactics. | Pierre-Marie Pédrot | 2016-09-08 |
| | * | | Unplugging Tacexpr in several interface files. | Pierre-Marie Pédrot | 2016-09-08 |
| |/ / |/| | |