From ffa57bae1e18fd52d63e8512a352ac63db15a7a9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 6 Aug 2009 19:00:11 +0000 Subject: - Cleaning phase of the interfaces of libnames.ml and nametab.ml (uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/interface/centaur.ml4 | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/interface/centaur.ml4') diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4 index f8c0887796..c8fc7bdf3a 100644 --- a/plugins/interface/centaur.ml4 +++ b/plugins/interface/centaur.ml4 @@ -146,7 +146,7 @@ let ctf_acknowledge_command request_id command_count opt_exn = g_count, !current_goal_index else (0, 0) - and statnum = Lib.current_command_label () + and statnum = Lib.current_state_label () and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0 and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in (ctf_header "acknowledge" request_id ++ @@ -409,12 +409,12 @@ let inspect n = (match oname, object_tag lobj with (sp,_), "VARIABLE" -> let (_, _, v) = Global.lookup_named (basename sp) in - add_search2 (Nametab.locate (qualid_of_sp sp)) v + add_search2 (Nametab.locate (qualid_of_path sp)) v | (sp,kn), "CONSTANT" -> let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in - add_search2 (Nametab.locate (qualid_of_sp sp)) typ + add_search2 (Nametab.locate (qualid_of_path sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> - add_search2 (Nametab.locate (qualid_of_sp sp)) + add_search2 (Nametab.locate (qualid_of_path sp)) (Pretyping.Default.understand Evd.empty (Global.env()) (RRef(dummy_loc, IndRef(kn,0)))) | _ -> failwith ("unexpected value 1 for "^ @@ -764,12 +764,12 @@ let full_name_of_ref r = | ConstRef _ -> str "CST" | IndRef _ -> str "IND" | ConstructRef _ -> str "CSR") - ++ str " " ++ (pr_sp (Nametab.sp_of_global r)) + ++ str " " ++ (pr_path (Nametab.path_of_global r)) (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *) let string_of_ref = (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*) - Depends.o Libnames.string_of_path Nametab.sp_of_global + Depends.o Libnames.string_of_path Nametab.path_of_global let print_depends compute_depends ptree = output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl()) -- cgit v1.2.3