| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Recognizing Z in romega up to conversion. |  Hugo Herbelin | 2017-11-23 |
| * | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin | 2017-11-23 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |