Small cleaning of printing coercion failures in Ltac interpretation.

Now we at least print the type of the offending object.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16657 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 24 insertions, 0 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 8e18be3d0c..98287d1842 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -49,6 +49,27 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2
 | _ -> false
 
+let rec pr_argument_type = function
+| IntOrVarArgType -> str "int_or_var"
+| IdentArgType true -> str "ident"
+| IdentArgType false -> str "pattern_ident"
+| VarArgType -> str "var"
+| RefArgType -> str "ref"
+| GenArgType -> str "genarg"
+| ConstrArgType -> str "constr"
+| ConstrMayEvalArgType -> str "constr_may_eval"
+| QuantHypArgType -> str "qhyp"
+| OpenConstrArgType _ -> str "open_constr"
+| ConstrWithBindingsArgType -> str "constr_with_bindings"
+| BindingsArgType -> str "bindings"
+| RedExprArgType -> str "redexp"
+| ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
+| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
+| PairArgType (t1, t2) ->
+    str "("++ pr_argument_type t1 ++ spc () ++
+    str "*" ++ spc () ++ pr_argument_type t2 ++ str ")"
+| ExtraArgType s -> str s
+
 type ('raw, 'glob, 'top) genarg_type = argument_type
 
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
diff --git a/lib/genarg.mli b/lib/genarg.mli
index b8dd08f960..e2654fcf57 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -210,6 +210,9 @@ type argument_type =
 
 val argument_type_eq : argument_type -> argument_type -> bool
 
+val pr_argument_type : argument_type -> Pp.std_ppcmds
+(** Print a human-readable representation for a given type. *)
+
 val genarg_tag : 'a generic_argument -> argument_type
 
 val unquote : ('a, 'co) abstract_argument_type -> argument_type