| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-04 | Fix #12011 ssreflect "rewrite in" with setoids | Gaëtan Gilbert | |
| ssreflect asks setoid rewrite to rewrite in goal "forall_special_name_ : T, _other_name_" Since this is a non dependent product, setoid rewrite converts that to "impl T _other_name_" and must be taught to restore the special name when unfolding impl. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |