diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e8a8dcb7c..b005aedf6 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -526,15 +526,16 @@ let pr_constraints printenv env evm = let explain_unsatisfiable_constraints env evd constr = let evm = Evarutil.nf_evars evd in + let undef = Evd.undefined_evars evm in match constr with | None -> str"Unable to satisfy the following constraints:" ++ fnl() ++ pr_constraints true env evm - | Some (evi, k) -> - explain_unsolvable_implicit env evi k None ++ fnl () ++ - if List.length (Evd.to_list evm) > 1 then + | Some (ev, k) -> + explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++ + if List.length (Evd.to_list undef) > 1 then str"With the following constraints:" ++ fnl() ++ - pr_constraints false env evm + pr_constraints false env (Evd.remove undef ev) else mt () let explain_mismatched_contexts env c i j = |