| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2018-05-17 | Introduce an option to allow nested lemma, and turn it off by default. | Théo Zimmermann | |
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2016-07-05 | congruence fix: test-suite code and update CHANGES | Matthieu Sozeau | |
| This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718. | |||
| 2016-07-04 | congruence/univs: properly refresh (fix #4609) | Matthieu Sozeau | |
| In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609. | |||
| 2015-10-07 | Fix bug #4069: f_equal regression. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |