| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Refine 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. | ||
| * | Adding variants enter_one and refine_one which assume that exactly one |  Hugo Herbelin | 2016-09-16 |
| | | | | | goal is under focus and which support returning a relevant output. | ||
| * | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | 2016-06-09 |
| | | |||
| * | Moving Refine to its proper module. | Pierre-Marie Pédrot | 2016-03-20 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |