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

1 files changed, 0 insertions, 23 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e3efd196c..89e2d7ddd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -348,29 +348,6 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
 
-(* extendable tactic arguments *)
-let rec pr_argument_type = function
-  (* Basic types *)
-  | IntOrVarArgType -> str"int-or-var"
-  | IdentArgType true -> str"ident"
-  | IdentArgType false -> str"pattern_ident"
-  | VarArgType -> str"var"
-  | RefArgType -> str"ref"
-  (* Specific types *)
-  | 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 ++ str" list"
-  | OptArgType t -> pr_argument_type t ++ str" opt"
-  | PairArgType (t1,t2) ->
-      str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")"
-  | ExtraArgType s -> str"\"" ++ str s ++ str "\""
-
 let pp_argument_type t = pp (pr_argument_type t)
 
 let pp_generic_argument arg =