| Commit message (Collapse) | 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 |
| Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |