diff options
| author | Guillaume Melquiond | 2014-06-16 16:34:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-06-16 16:34:17 +0200 |
| commit | 7e69422ea16c9e323d02fdd7c4927750b40bd2cf (patch) | |
| tree | c7422fd92bfd2c9f9e1604419b830e106a8f649d | |
| parent | f1ecf669d82c8b6d05068e12f96f993982ecb533 (diff) | |
Fix spacing in error message.
| -rw-r--r-- | toplevel/himsg.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 41ce6f1da0..90e3588284 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -263,9 +263,8 @@ let explain_unification_error env sigma p1 p2 = function | InstanceNotSameType (evk,env,t,u) -> let t, u = pr_explicit env t u in spc () ++ str "(unable to find a well-typed instantiation for " ++ - quote (pr_existential_key evk) ++ str ":" ++ spc () ++ - str "cannot unify" ++ t ++ spc () ++ str "and" ++ spc () ++ - u ++ str ")" + quote (pr_existential_key evk) ++ strbrk ": cannot unify " ++ + t ++ strbrk " and " ++ u ++ str ")" | UnifUnivInconsistency p -> if !Constrextern.print_universes then spc () ++ str "(Universe inconsistency: " ++ |