| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-08-26 | Modify lia to work with -mangle-names | Jasper Hugunin | |
| We used to be refreshing the names for intros but not using the refreshed names. The same pattern of `intro_using` (which is what `intros ?name` effectively is) messing things up as in coq/coq#12881. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |