From 39a10cba3d610c6f12438084c5de7c1217c8fe94 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Jun 2018 11:44:32 +0200
Subject: Checking if low-level name printers are used on purpose or not.

In particular we check if really used for internal debugging purpose
or to display a message to the user. In the latter case, we replace it
(when possible) by a higher-level printer (e.g. printing foo instead
of Top.foo). In the former case, we clarify that the use is a
debugging use.

Still not perfect (see a few FIXME).
---
 tactics/tacticals.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 837865e644..878e2b1f01 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -655,12 +655,11 @@ module New = struct
       | _ ->
 	  let name_elim =
 	    match EConstr.kind sigma elim with
-	    | Const (kn, _) -> Constant.to_string kn
-	    | Var id -> Id.to_string id
-	    | _ -> "\b"
+            | Const _ | Var _ -> str " " ++ print_constr_env (pf_env gl) sigma elim
+            | _ -> mt ()
 	  in
 	  user_err ~hdr:"Tacticals.general_elim_then_using"
-            (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
+            (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
     let branchsigns = compute_constructor_signatures ~rec_flag ind in
-- 
cgit v1.2.3