Merge PR #8534: Checking if low-level name printers are used on purpose or not

19 files changed, 62 insertions, 45 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index 74cf237763..b172acb126 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -183,7 +183,7 @@ let lookup_mind kn env =
 
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
-    Printf.ksprintf anomaly ("Inductive %s is already defined.")
+    Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 8f11e01c33..1fd86bc368 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -595,8 +595,12 @@ let check_subtyping cumi paramsctxt env inds =
 (************************************************************************)
 (************************************************************************)
 
+let print_mutind ind =
+  let kn = MutInd.user ind in
+  str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn))
+
 let check_inductive env kn mib =
-  Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
+  Flags.if_verbose Feedback.msg_notice (str "  checking mutind block: " ++ print_mutind kn);
   (* check mind_constraints: should be consistent with env *)
   let env0 =
     match mib.mind_universes with
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 138fe8bc95..e4c3f4ae4b 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -158,7 +158,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
+      failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
   in
   type_of_inductive_knowing_parameters env (specif,u) paramstyp
 
@@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) =
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
+      failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
   in
   type_of_constructor (c,u) specif
 
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 47cfeb98d7..ea126e2756 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -10,7 +10,7 @@ let ppripos (ri,pos) =
   | Reloc_annot a ->
       let sp,i = a.ci.ci_ind in
       print_string
-	("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
+        ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
diff --git a/engine/termops.ml b/engine/termops.ml
index 156d1370e3..710743e92d 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -49,6 +49,8 @@ let pr_puniverses p u =
   if Univ.Instance.is_empty u then p 
   else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
 
+(* Minimalistic constr printer, typically for debugging *)
+
 let rec pr_constr c = match kind c with
   | Rel n -> str "#"++int n
   | Meta n -> str "Meta(" ++ int n ++ str ")"
diff --git a/engine/termops.mli b/engine/termops.mli
index b967bb6abb..9ce2db9234 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -311,11 +311,17 @@ val pr_metaset : Metaset.t -> Pp.t
 val pr_evar_universe_context : UState.t -> Pp.t
 val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
 
-(** debug printer: do not use to display terms to the casual user... *)
+(** Internal hook to register user-level printer *)
 
 val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+
+(** User-level printers *)
+
 val print_constr     : constr -> Pp.t
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+
+(** debug printer: do not use to display terms to the casual user... *)
+
 val print_named_context : env -> Pp.t
 val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
 val print_rel_context : env -> Pp.t
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ddc0a5c000..3996a1756c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -102,7 +102,7 @@ let _show_inactive_notations () =
       (function
        | NotationRule (scopt, ntn) ->
          Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
-       | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn)))
+       | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
       !inactive_notations_table
 
 let deactivate_notation nr =
@@ -135,8 +135,9 @@ let reactivate_notation nr =
                              ++ str "is already active" ++ show_scope scopt ++
   str ".")
     | SynDefRule kn ->
+       let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
        Feedback.msg_warning
-         (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn)
+         (str "Notation" ++ spc () ++ str s
           ++ spc () ++ str "is already active.")
 
 
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index edce9367fc..8ac3538fc5 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -29,7 +29,7 @@ and translate_field prefix mp env acc (l,x) =
   | SFBconst cb ->
      let con = Constant.make3 mp DirPath.empty l in
      (if !Flags.debug then
-	let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
+        let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
 	Feedback.msg_debug (Pp.str msg));
      compile_constant_field env prefix con acc cb
   | SFBmind mb ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f39dde772a..47247ff25e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -103,12 +103,7 @@ let inline_side_effects env body ctx side_eff =
   if List.is_empty side_eff then (body, ctx, sigs)
   else
     (** Second step: compute the lifts and substitutions to apply *)
-    let cname c =
-      let name = Constant.to_string c in
-      let map c = if c == '.' || c == '#' then '_' else c in
-      let name = String.map map name in
-      Name (Id.of_string name)
-    in
+    let cname c = Name (Label.to_id (Constant.label c)) in
     let fold (subst, var, ctx, args) (c, cb, b) =
       let (b, opaque) = match cb.const_body, b with
       | Def b, _ -> (Mod_subst.force_constr b, false)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 803d35d07c..b219ee25ca 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -272,6 +272,8 @@ let string_of_genarg_arg (ArgumentType arg) =
       in
       pr_sequence pr prods
     with Not_found ->
+      (* FIXME: This key, moreover printed with a low-level printer,
+         has no meaning user-side *)
       KerName.print key
 
   let pr_alias_gen pr_gen lev key l =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 67ffae59cc..9f34df4608 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1298,7 +1298,7 @@ and tactic_of_value ist vle =
        match appl with
          UnnamedAppl -> "An unnamed user-defined tactic"
        | GlbAppl apps ->
-          let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in
+          let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in
           match nms with
             []    -> assert false
           | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index fc24e9b3a9..265909980b 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -187,7 +187,7 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> debug_cbv:=a);
 }
 
-let pr_key = function
+let debug_pr_key = function
   | ConstKey (sp,_) -> Names.Constant.print sp
   | VarKey id -> Names.Id.print id
   | RelKey n -> Pp.(str "REL_" ++ int n)
@@ -320,14 +320,14 @@ and norm_head_ref k info env stack normt =
   if red_set_ref (info_flags info.infos) normt then
     match ref_value_cache info.infos info.tab normt with
       | Some body ->
-         if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
+         if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
          strip_appl (shift_value k body) stack
       | None ->
-         if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+         if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
          (VAL(0,make_constr_ref k normt),stack)
   else
     begin
-      if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+      if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
       (VAL(0,make_constr_ref k normt),stack)
     end
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ec0ff73062..b040e63cd2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches =
           not (has_dependent_elim mib) then
        user_err ~hdr:"make_case_or_project"
                     Pp.(str"Dependent case analysis not allowed" ++
-                     str" on inductive type " ++ Names.MutInd.print (fst ind))
+                     str" on inductive type " ++ print_constr_env env sigma (mkInd ind))
      in
      let branch = branches.(0) in
      let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bd41e61b34..77ad96d2cf 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -334,19 +334,19 @@ let error_not_structure ref description =
   user_err ~hdr:"object_declare"
     (str"Could not declare a canonical structure " ++
        (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
-          str(description)))
+          description))
 
 let check_and_decompose_canonical_structure ref =
   let sp =
     match ref with
       ConstRef sp -> sp
-    |  _ -> error_not_structure ref "Expected an instance of a record or structure."
+    |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
   in
   let env = Global.env () in
   let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
-    | None -> error_not_structure ref "Could not find its value in the global environment." in
+    | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
   let env = Global.env () in
   let evd = Evd.from_env env in
   let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in
@@ -354,18 +354,18 @@ let check_and_decompose_canonical_structure ref =
   let f,args = match kind body with
     | App (f,args) -> f,args
     | _ ->
-       error_not_structure ref "Expected a record or structure constructor applied to arguments." in
+       error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in
   let indsp = match kind f with
     | Construct ((indsp,1),u) -> indsp
-    | _ -> error_not_structure ref "Expected an instance of a record or structure." in
+    | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in
   let s =
     try lookup_structure indsp
     with Not_found ->
       error_not_structure ref
-        ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in
+        (str "Could not find the record or structure " ++ Termops.print_constr (EConstr.mkInd indsp)) in
   let ntrue_projs = List.count snd s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
-    error_not_structure ref "Got too few arguments to the record or structure constructor.";
+    error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (sp,indsp)
 
 let declare_canonical_structure ref =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f4c8a6cd66..a0d20b7ce4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -341,6 +341,7 @@ struct
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
   and 'a t = 'a member list
 
+  (* Debugging printer *)
   let rec pr_member pr_c member =
     let open Pp in
     let pr_c x = hov 1 (pr_c x) in
@@ -351,7 +352,7 @@ struct
 	 prvect_with_sep (pr_bar) pr_c br
        ++ str ")"
     | Proj (p,cst) ->
-      str "ZProj(" ++ Constant.print (Projection.constant p) ++ str ")"
+      str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
        str "ZFix(" ++ Termops.pr_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
@@ -368,11 +369,11 @@ struct
     let open Pp in
       match c with
       | Cst_const (c, u) ->
-	if Univ.Instance.is_empty u then Constant.print c
-	else str"(" ++ Constant.print c ++ str ", " ++ 
+        if Univ.Instance.is_empty u then Constant.debug_print c
+        else str"(" ++ Constant.debug_print c ++ str ", " ++
 	  Univ.Instance.pr Univ.Level.pr u ++ str")"
       | Cst_proj p ->
-	str".(" ++ Constant.print (Projection.constant p) ++ str")"
+        str".(" ++ Constant.debug_print (Projection.constant p) ++ str")"
 
   let empty = []
   let is_empty = CList.is_empty
diff --git a/printing/printer.ml b/printing/printer.ml
index 67d71332b0..5ca330d377 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -944,9 +944,16 @@ let pr_assumptionset env sigma s =
     let safe_pr_constant env kn =
       try pr_constant env kn
       with Not_found ->
+        (* FIXME? *)
 	let mp,_,lab = Constant.repr3 kn in
         str (ModPath.to_string mp) ++ str "." ++ Label.print lab
     in
+    let safe_pr_inductive env kn =
+      try pr_inductive env (kn,0)
+      with Not_found ->
+        (* FIXME? *)
+        MutInd.print kn
+    in
     let safe_pr_ltype env sigma typ =
       try str " : " ++ pr_ltype_env env sigma typ
       with e when CErrors.noncritical e -> mt ()
@@ -961,7 +968,7 @@ let pr_assumptionset env sigma s =
       | Constant kn ->
           safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
       | Positive m ->
-          hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
+          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
       | Guarded kn ->
           hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
     in
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
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
index 7326f137c2..8a00cd3fe5 100644
--- a/test-suite/output/ltac_missing_args.out
+++ b/test-suite/output/ltac_missing_args.out
@@ -1,25 +1,25 @@
 The command has indeed failed with message:
-The user-defined tactic "Top.foo" was not fully applied:
+The user-defined tactic "foo" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.bar" was not fully applied:
+The user-defined tactic "bar" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.bar" was not fully applied:
+The user-defined tactic "bar" was not fully applied:
 There are missing arguments for variables y and _,
 an argument was provided for variable x.
 The command has indeed failed with message:
-The user-defined tactic "Top.baz" was not fully applied:
+The user-defined tactic "baz" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.qux" was not fully applied:
+The user-defined tactic "qux" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.mydo" was not fully applied:
+The user-defined tactic "mydo" was not fully applied:
 There is a missing argument for variable _,
 no arguments at all were provided.
 The command has indeed failed with message:
@@ -31,7 +31,7 @@ An unnamed user-defined tactic was not fully applied:
 There is a missing argument for variable _,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.rec" was not fully applied:
+The user-defined tactic "rec" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index e33aa38173..3bf3925b4b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -543,7 +543,7 @@ let eqI ind l =
   and e, eff = 
     try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff 
     with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
-      (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed.");
+      (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
   in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
 
 (**********************************************************************)