| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode |  Matthieu Sozeau | 2014-09-15 |
| | | | | | | | | | | | | | | of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases). | ||
| * | Avoid backtracking in typeclass search if a solution for a closed | Matthieu Sozeau | 2014-09-15 |
| | | | | | | non-dependent or propositional constraint has already been found (same behavior as before previous patch). | ||
| * | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau | 2014-09-15 |
| Add a global option to check for multiple solutions and fail in that case. Add another flag to declare classes as having unique instances (not checked but assumed correct, avoiding some backtracking). | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |