diff options
-rw-r--r-- | API/API.mli | 40 | ||||
-rw-r--r-- | library/nametab.ml | 47 | ||||
-rw-r--r-- | library/nametab.mli | 9 | ||||
-rw-r--r-- | plugins/ltac/ltac_plugin.mlpack | 4 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/pptactic.mli | 2 | ||||
-rw-r--r-- | plugins/ltac/tacentries.ml | 10 | ||||
-rw-r--r-- | plugins/ltac/tacenv.ml | 44 | ||||
-rw-r--r-- | plugins/ltac/tacenv.mli | 10 | ||||
-rw-r--r-- | plugins/ltac/tacexpr.mli | 3 | ||||
-rw-r--r-- | plugins/ltac/tacintern.ml | 6 | ||||
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
-rw-r--r-- | plugins/ssr/ssrparser.ml4 | 4 | ||||
-rw-r--r-- | printing/prettyp.ml | 11 |
14 files changed, 109 insertions, 87 deletions
diff --git a/API/API.mli b/API/API.mli index 3ed326ff0..e2cb70583 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1795,6 +1795,7 @@ sig val pr_path : full_path -> Pp.t val make_path : Names.DirPath.t -> Names.Id.t -> full_path val eq_full_path : full_path -> full_path -> bool + val repr_path : full_path -> Names.DirPath.t * Names.Id.t val dirpath : full_path -> Names.DirPath.t val path_of_string : string -> full_path @@ -1935,24 +1936,19 @@ module Nametab : sig exception GlobalizationError of Libnames.qualid - type ltac_constant = Names.KerName.t - val global : Libnames.reference -> Globnames.global_reference val global_of_path : Libnames.full_path -> Globnames.global_reference val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid val path_of_global : Globnames.global_reference -> Libnames.full_path val locate_extended : Libnames.qualid -> Globnames.extended_global_reference val full_name_module : Libnames.qualid -> Names.DirPath.t - val locate_tactic : Libnames.qualid -> Names.KerName.t val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.t - val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid val basename_of_global : Globnames.global_reference -> Names.Id.t type visibility = | Until of int | Exactly of int - val push_tactic : visibility -> Libnames.full_path -> Names.KerName.t -> unit val error_global_not_found : ?loc:Loc.t -> Libnames.qualid -> 'a val shortest_qualid_of_module : Names.ModPath.t -> Libnames.qualid val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t @@ -1960,6 +1956,40 @@ sig val dirpath_of_global : Globnames.global_reference -> Names.DirPath.t val locate : Libnames.qualid -> Globnames.global_reference val locate_constant : Libnames.qualid -> Names.Constant.t + + (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *) + + module type UserName = sig + type t + val equal : t -> t -> bool + val to_string : t -> string + val repr : t -> Names.Id.t * Names.Id.t list + end + + module type EqualityType = + sig + type t + val equal : t -> t -> bool + end + + module type NAMETREE = sig + type elt + type t + type user_name + + val empty : t + val push : visibility -> user_name -> elt -> t -> t + val locate : Libnames.qualid -> t -> elt + val find : user_name -> t -> elt + val exists : user_name -> t -> bool + val user_name : Libnames.qualid -> t -> user_name + val shortest_qualid : Names.Id.Set.t -> user_name -> t -> Libnames.qualid + val find_prefixes : Libnames.qualid -> t -> elt list + end + + module Make (U : UserName) (E : EqualityType) : + NAMETREE with type user_name = U.t and type elt = E.t + end module Global : diff --git a/library/nametab.ml b/library/nametab.ml index 68fdbb4f3..0ec4a37cd 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -19,10 +19,6 @@ exception GlobalizationError of qualid let error_global_not_found ?loc q = Loc.raise ?loc (GlobalizationError q) -(* Kinds of global names *) - -type ltac_constant = kernel_name - (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object is loaded inside a module @@ -274,19 +270,14 @@ struct end module ExtRefEqual = ExtRefOrdered -module KnEqual = Names.KerName module MPEqual = Names.ModPath module ExtRefTab = Make(FullPath)(ExtRefEqual) -module KnTab = Make(FullPath)(KnEqual) module MPTab = Make(FullPath)(MPEqual) type ccitab = ExtRefTab.t let the_ccitab = ref (ExtRefTab.empty : ccitab) -type kntab = KnTab.t -let the_tactictab = ref (KnTab.empty : kntab) - type mptab = MPTab.t let the_modtypetab = ref (MPTab.empty : mptab) @@ -327,10 +318,6 @@ let the_modrevtab = ref (MPmap.empty : mprevtab) type mptrevtab = full_path MPmap.t let the_modtyperevtab = ref (MPmap.empty : mptrevtab) -type knrevtab = full_path KNmap.t -let the_tacticrevtab = ref (KNmap.empty : knrevtab) - - (* Push functions *********************************************************) (* This is for permanent constructions (never discharged -- but with @@ -368,13 +355,6 @@ let push_modtype vis sp kn = the_modtypetab := MPTab.push vis sp kn !the_modtypetab; the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab -(* This is for tactic definition names *) - -let push_tactic vis sp kn = - the_tactictab := KnTab.push vis sp kn !the_tactictab; - the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab - - (* This is to remember absolute Section/Module names and to avoid redundancy *) let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; @@ -402,8 +382,6 @@ let locate_syndef qid = match locate_extended qid with let locate_modtype qid = MPTab.locate qid !the_modtypetab let full_name_modtype qid = MPTab.user_name qid !the_modtypetab -let locate_tactic qid = KnTab.locate qid !the_tactictab - let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = @@ -428,8 +406,6 @@ let locate_all qid = let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab -let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab - let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab @@ -471,8 +447,6 @@ let exists_module = exists_dir let exists_modtype sp = MPTab.exists sp !the_modtypetab -let exists_tactic kn = KnTab.exists kn !the_tactictab - (* Reverse locate functions ***********************************************) let path_of_global ref = @@ -492,9 +466,6 @@ let path_of_syndef kn = let dirpath_of_module mp = MPmap.find mp !the_modrevtab -let path_of_tactic kn = - KNmap.find kn !the_tacticrevtab - let path_of_modtype mp = MPmap.find mp !the_modtyperevtab @@ -519,10 +490,6 @@ let shortest_qualid_of_modtype kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_tactic kn = - let sp = KNmap.find kn !the_tacticrevtab in - KnTab.shortest_qualid Id.Set.empty sp !the_tactictab - let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> @@ -541,28 +508,24 @@ let global_inductive r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * mptab * kntab - * globrevtab * mprevtab * mptrevtab * knrevtab +type frozen = ccitab * dirtab * mptab + * globrevtab * mprevtab * mptrevtab let freeze _ : frozen = !the_ccitab, !the_dirtab, !the_modtypetab, - !the_tactictab, !the_globrevtab, !the_modrevtab, - !the_modtyperevtab, - !the_tacticrevtab + !the_modtyperevtab -let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) = +let unfreeze (ccit,dirt,mtyt,globr,modr,mtyr) = the_ccitab := ccit; the_dirtab := dirt; the_modtypetab := mtyt; - the_tactictab := tact; the_globrevtab := globr; the_modrevtab := modr; - the_modtyperevtab := mtyr; - the_tacticrevtab := tacr + the_modtyperevtab := mtyr let _ = Summary.declare_summary "names" diff --git a/library/nametab.mli b/library/nametab.mli index 025a63b1c..3a380637c 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -78,10 +78,6 @@ val push_modtype : visibility -> full_path -> module_path -> unit val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit -type ltac_constant = kernel_name -val push_tactic : visibility -> full_path -> ltac_constant -> unit - - (** {6 The following functions perform globalization of qualified names } *) (** These functions globalize a (partially) qualified name or fail with @@ -95,7 +91,6 @@ val locate_modtype : qualid -> module_path val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path val locate_section : qualid -> DirPath.t -val locate_tactic : qualid -> ltac_constant (** These functions globalize user-level references into global references, like [locate] and co, but raise a nice error message @@ -109,7 +104,6 @@ val global_inductive : reference -> inductive val locate_all : qualid -> global_reference list val locate_extended_all : qualid -> extended_global_reference list -val locate_extended_all_tactic : qualid -> ltac_constant list val locate_extended_all_dir : qualid -> global_dir_reference list val locate_extended_all_modtype : qualid -> module_path list @@ -125,7 +119,6 @@ val exists_modtype : full_path -> bool val exists_dir : DirPath.t -> bool val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) -val exists_tactic : full_path -> bool (** deprecated synonym of [exists_dir] *) (** {6 These functions locate qualids into full user names } *) @@ -144,7 +137,6 @@ val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path val dirpath_of_module : module_path -> DirPath.t val path_of_modtype : module_path -> full_path -val path_of_tactic : ltac_constant -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) @@ -166,7 +158,6 @@ val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : module_path -> qualid val shortest_qualid_of_module : module_path -> qualid -val shortest_qualid_of_tactic : ltac_constant -> qualid (** Deprecated synonyms *) diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack index 12b4c81fc..3972b7aac 100644 --- a/plugins/ltac/ltac_plugin.mlpack +++ b/plugins/ltac/ltac_plugin.mlpack @@ -1,9 +1,9 @@ Tacarg +Tacsubst +Tacenv Pptactic Pltac Taccoerce -Tacsubst -Tacenv Tactic_debug Tacintern Tacentries diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d8bd16620..d588c888c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -336,7 +336,7 @@ type 'a extra_genarg_printer = let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn else try - pr_qualid (Nametab.shortest_qualid_of_tactic kn) + pr_qualid (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) str "<" ++ KerName.print kn ++ str ">" diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index c79d5b389..d9da954fe 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -93,7 +93,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t val pr_alias : (Val.t -> Pp.t) -> int -> Names.KerName.t -> Val.t list -> Pp.t -val pr_ltac_constant : Nametab.ltac_constant -> Pp.t +val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : raw_tactic_expr -> Pp.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a8d518fbd..8573da19f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -409,7 +409,7 @@ let create_ltac_quotation name cast (e, l) = type tacdef_kind = | NewTac of Id.t - | UpdateTac of Nametab.ltac_constant + | UpdateTac of Tacexpr.ltac_constant let is_defined_tac kn = try ignore (Tacenv.interp_ltac kn); true with Not_found -> false @@ -441,7 +441,7 @@ let register_ltac local tacl = | Tacexpr.TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in let kn = - try Nametab.locate_tactic (snd (qualid_of_reference ident)) + try Tacenv.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> CErrors.user_err ?loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") @@ -464,7 +464,7 @@ let register_ltac local tacl = let defs () = (** Register locally the tactic to handle recursivity. This function affects the whole environment, so that we transactify it afterwards. *) - let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in + let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in let () = List.iter iter_rec recvars in List.map map rfun in @@ -475,7 +475,7 @@ let register_ltac local tacl = Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> Tacenv.redefine_ltac local kn tac; - let name = Nametab.shortest_qualid_of_tactic kn in + let name = Tacenv.shortest_qualid_of_tactic kn in Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") in List.iter iter defs @@ -488,7 +488,7 @@ let print_ltacs () = let entries = List.sort sort entries in let map (kn, entry) = let qid = - try Some (Nametab.shortest_qualid_of_tactic kn) + try Some (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> None in match qid with diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 13b44f0e2..8c59a36fa 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -11,6 +11,42 @@ open Pp open Names open Tacexpr +(** Nametab for tactics *) + +(** TODO: Share me somewhere *) +module FullPath = +struct + open Libnames + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (DirPath.repr dir) +end + +module KnTab = Nametab.Make(FullPath)(KerName) + +let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty) + +let push_tactic vis sp kn = + let (tab, revtab) = !tactic_tab in + let tab = KnTab.push vis sp kn tab in + let revtab = KNmap.add kn sp revtab in + tactic_tab := (tab, revtab) + +let locate_tactic qid = KnTab.locate qid (fst !tactic_tab) + +let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab) + +let exists_tactic kn = KnTab.exists kn (fst !tactic_tab) + +let path_of_tactic kn = KNmap.find kn (snd !tactic_tab) + +let shortest_qualid_of_tactic kn = + let sp = KNmap.find kn (snd !tactic_tab) in + KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab) + (** Tactic notations (TacAlias) *) type alias = KerName.t @@ -103,19 +139,19 @@ let replace kn path t = let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Until i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Exactly i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> - let () = Nametab.push_tactic (Until 1) sp kn in + let () = push_tactic (Until 1) sp kn in add kn b t | Some kn0 -> replace kn0 kn t @@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) = let classify_md (local, _, _, _ as o) = Substitute o -let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 958109e5a..4ecc978fe 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -7,11 +7,21 @@ (************************************************************************) open Names +open Libnames open Tacexpr open Geninterp (** This module centralizes the various ways of registering tactics. *) +(** {5 Tactic naming} *) + +val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit +val locate_tactic : qualid -> ltac_constant +val locate_extended_all_tactic : qualid -> ltac_constant list +val exists_tactic : full_path -> bool +val path_of_tactic : ltac_constant -> full_path +val shortest_qualid_of_tactic : ltac_constant -> qualid + (** {5 Tactic notations} *) type alias = KerName.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 64da097de..2c36faeff 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -10,13 +10,14 @@ open Loc open Names open Constrexpr open Libnames -open Nametab open Genredexpr open Genarg open Pattern open Misctypes open Locus +type ltac_constant = KerName.t + type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index fc6ee6aab..99d7684d3 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -118,7 +118,7 @@ let intern_constr_reference strict ist = function let intern_isolated_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[])) + TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) @@ -137,7 +137,7 @@ let intern_isolated_tactic_reference strict ist r = let intern_applied_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - ArgArg (loc,locate_tactic qid) + ArgArg (loc,Tacenv.locate_tactic qid) let intern_applied_tactic_reference ist r = (* An ltac reference *) @@ -722,7 +722,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try - let kn = Nametab.locate_tactic id in + let kn = Tacenv.locate_tactic id in let entries = Tacenv.ltac_entries () in let tac = KNmap.find kn entries in let filter mp = diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index cf5fdf318..d37c676e3 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -814,8 +814,8 @@ let ssr_n_tac seed n gl = let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in let fail msg = CErrors.user_err (Pp.str msg) in let tacname = - try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) - with Not_found -> try Nametab.locate_tactic (ssrqid name) + try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) + with Not_found -> try Tacenv.locate_tactic (ssrqid name) with Not_found -> if n = -1 then fail "The ssreflect library was not loaded" else fail ("The tactic "^name^" was not found") in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 1e1a986da..7b591fead 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1554,8 +1554,8 @@ END let ssrautoprop gl = try let tacname = - try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) - with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in + try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) + with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 09859157c..b2e7fe447 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -309,7 +309,6 @@ type logical_name = | Dir of global_dir_reference | Syntactic of kernel_name | ModuleType of module_path - | Tactic of Nametab.ltac_constant | Undefined of qualid let locate_any_name ref = @@ -344,8 +343,6 @@ let pr_located_qualid = function str s ++ spc () ++ pr_dirpath dir | ModuleType mp -> str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) - | Tactic kn -> - str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn) | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." @@ -383,10 +380,6 @@ let locate_term qid = in List.map expand (Nametab.locate_extended_all qid) -let locate_tactic qid = - let all = Nametab.locate_extended_all_tactic qid in - List.map (fun kn -> (Tactic kn, Nametab.shortest_qualid_of_tactic kn)) all - let locate_module qid = let all = Nametab.locate_extended_all_dir qid in let map dir = match dir with @@ -411,7 +404,6 @@ let locate_modtype qid = let print_located_qualid name flags ref = let (loc,qid) = qualid_of_reference ref in let located = [] in - let located = if List.mem `LTAC flags then locate_tactic qid @ located else located in let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in let located = if List.mem `MODULE flags then locate_module qid @ located else located in let located = if List.mem `TERM flags then locate_term qid @ located else located in @@ -765,7 +757,6 @@ let print_any_name = function | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp | Dir _ -> mt () | ModuleType mp -> print_modtype mp - | Tactic kn -> mt () (** TODO *) | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in @@ -822,7 +813,7 @@ let print_about_any ?loc k = v 0 ( print_syntactic_def kn ++ fnl () ++ hov 0 (str "Expands to: " ++ pr_located_qualid k)) - | Dir _ | ModuleType _ | Tactic _ | Undefined _ -> + | Dir _ | ModuleType _ | Undefined _ -> hov 0 (pr_located_qualid k) let print_about = function |