diff options
| author | Hugo Herbelin | 2016-04-26 05:53:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:43:29 +0200 |
| commit | 09d6ce5340a818f24a85d568aab6502233e10273 (patch) | |
| tree | 9c5e976104b503017886a76c4f54c8fbcbed821d | |
| parent | 63ac502a4ea7f5c81346deeecfcf0d69d063a130 (diff) | |
Fixing space in an error message.
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 789e8d64b4..4a33549f94 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -168,7 +168,7 @@ module Value = struct let pr_v = Pptactic.pr_value Pptactic.ltop v in let Val.Dyn (tag, _) = v in let tag = Val.pr tag in - errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag + errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag ++ str " while type " ++ Val.pr wit ++ str " was expected.") let unbox wit v ans = match ans with |