| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-23 | Fix #8937: inductive conversion in coqchk subtyping | Gaëtan Gilbert | |
| As far as I can tell this is similar to what coqtop does. Delta resolvers are complicated so I may be mistaken. The important part is to avoid losing the modified delta resolver returned by strengthen_and_subst in check_mexpr. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |