diff options
| author | Hugo Herbelin | 2014-12-03 14:48:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-03 19:26:16 +0100 |
| commit | 34bb77c953e917f5fbff489c5758abcbadc22224 (patch) | |
| tree | d92ff3dbde50be1227891b7dde96a1ee3951c6ca | |
| parent | dfeaea43d9e692984cf430f4f19ec527625586ea (diff) | |
Slight improving of a unification error message.
| -rw-r--r-- | toplevel/himsg.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 421a975f17..9aa1486405 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -293,8 +293,9 @@ let explain_unification_error env sigma p1 p2 = function | InstanceNotSameType (evk,env,t,u) -> let t, u = pr_explicit env sigma t u in spc () ++ str "(unable to find a well-typed instantiation for " ++ - quote (pr_existential_key sigma evk) ++ strbrk ": cannot unify " ++ - t ++ strbrk " and " ++ u ++ str ")" + quote (pr_existential_key sigma evk) ++ + strbrk ": cannot ensure that " ++ + t ++ strbrk " is a subtype of " ++ u ++ str ")" | UnifUnivInconsistency p -> if !Constrextern.print_universes then spc () ++ str "(Universe inconsistency: " ++ |