| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Contradiction API using EConstr. |  Pierre-Marie Pédrot | 2017-02-14 |
| | | |||
| * | Equality API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | |||
| * | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | |||
| * | Clenv 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 |
| | | | | | | | | | | This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. | ||
| * | Introducing a new EConstr.t type to perform the nf_evar operation on demand. | Pierre-Marie Pédrot | 2016-11-08 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |