diff options
| author | Hugo Herbelin | 2018-04-19 08:05:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-04-19 08:05:31 +0200 |
| commit | 5f9df6d084bb24ea9b26a74387b79656e4123ee0 (patch) | |
| tree | 9bba8f5634df649e281e237495de999d36a1de35 | |
| parent | 513884e806a4db39ae6402333833ecc4f70a0fdc (diff) | |
Allowing formatting break around a printed type.
| -rw-r--r-- | src/tac2intern.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/tac2intern.ml b/src/tac2intern.ml index b1dd8f7f51..99965c4ed5 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -356,8 +356,8 @@ let rec unify0 env t1 t2 = match kind env t1, kind env t2 with let unify ?loc env t1 t2 = try unify0 env t1 t2 with CannotUnify (u1, u2) -> - user_err ?loc (str "This expression has type " ++ pr_glbtype env t1 ++ - str " but an expression was expected of type " ++ pr_glbtype env t2) + user_err ?loc (str "This expression has type" ++ spc () ++ pr_glbtype env t1 ++ + spc () ++ str "but an expression was expected of type" ++ spc () ++ pr_glbtype env t2) let unify_arrow ?loc env ft args = let ft0 = ft in @@ -372,11 +372,11 @@ let unify_arrow ?loc env ft args = iter ft args true | GTypRef _, _ :: _ -> if is_fun then - user_err ?loc (str "This function has type " ++ pr_glbtype env ft0 ++ - str " and is applied to too many arguments") + user_err ?loc (str "This function has type" ++ spc () ++ pr_glbtype env ft0 ++ + spc () ++ str "and is applied to too many arguments") else - user_err ?loc (str "This expression has type " ++ pr_glbtype env ft0 ++ - str " and is not a function") + user_err ?loc (str "This expression has type" ++ spc () ++ pr_glbtype env ft0 ++ + spc () ++ str "and is not a function") in iter ft args false @@ -475,13 +475,13 @@ let check_elt_empty loc env t = match kind env t with | GTypVar _ -> user_err ?loc (str "Cannot infer an empty type for this expression") | GTypArrow _ | GTypRef (Tuple _, _) -> - user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type") + user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type") | GTypRef (Other kn, _) -> let def = Tac2env.interp_type kn in match def with | _, GTydAlg { galg_constructors = [] } -> kn | _ -> - user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type") + user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type") let check_unit ?loc t = let env = empty_env () in |