| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-23 | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin | |
| 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. | |||
| 2016-11-17 | Add test suite files for 4700-4785 | Jason Gross | |
| I didn't add any test-cases for timing-based bugs (4707, 4768, 4776, 4777, 4779, 4783), nor CoqIDE bugs (4700, 4751, 4752, 4756), nor bugs about printing (4709, 4711, 4720, 4723, 4734, 4736, 4738, 4741, 4743, 4748, 4749, 4750, 4757, 4758, 4765, 4784). I'm not sure what to do with 4712, 4714, 4732, 4740. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |