diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 15:42:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 15:48:32 +0200 |
| commit | 2ac8e0edebe0d9a6bde4d997327dbd2ffcde08b6 (patch) | |
| tree | b144dcb1689899b5135289903932b18de55d9904 /toplevel/himsg.ml | |
| parent | 86c6649382bb9e42281ffe956c627c6d3987559b (diff) | |
- Allow parsing of @const@{instance} for specifying universe instances of polymorphic
constants.
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 9d6e9756d..db74e5aa1 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -861,7 +861,11 @@ let explain_unsatisfiable_constraints env evd constr comp = | None -> Typeclasses.is_resolvable evi | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp in - let undef = Evar.Map.filter is_kept undef in + let undef = + let m = Evar.Map.filter is_kept undef in + if Evar.Map.is_empty m then undef + else m + in match constr with | None -> str "Unable to satisfy the following constraints:" ++ fnl () ++ |