diff options
| author | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
| commit | e34d7cbcb5ee5c8888efef439ef264ce01a20824 (patch) | |
| tree | 0aa9dee30e64daca85cd3de427d47166bb345736 /ltac | |
| parent | 5e62bd67ca3cf35e4d1dd4a9c8f00c419dd668dd (diff) | |
Revert "Fixing space in an error message."
This reverts commit e0fd6e50800bc5aec4eafddd315941d6f7bc6efc.
Diffstat (limited to 'ltac')
| -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 0c9d7ff801..b742bb328d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -151,7 +151,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 " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.") let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> |