From 1a6a26d29252da54b86bf663a66ddd909905d1cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 3 Oct 2017 14:06:29 +0200 Subject: Moving the Ltac-specific part of the nametab to the Ltac plugin. For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit. --- printing/prettyp.ml | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) (limited to 'printing/prettyp.ml') 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 -- cgit v1.2.3