diff options
Diffstat (limited to 'plugins/interface')
| -rw-r--r-- | plugins/interface/centaur.ml4 | 12 | ||||
| -rw-r--r-- | plugins/interface/coqparser.ml | 2 | ||||
| -rw-r--r-- | plugins/interface/name_to_ast.ml | 16 | ||||
| -rw-r--r-- | plugins/interface/name_to_ast.mli | 2 |
4 files changed, 10 insertions, 22 deletions
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()) diff --git a/plugins/interface/coqparser.ml b/plugins/interface/coqparser.ml index a63e18d27e..df5e66b50f 100644 --- a/plugins/interface/coqparser.ml +++ b/plugins/interface/coqparser.ml @@ -335,7 +335,7 @@ let print_version_action () = let load_syntax_action reqid module_name = msg (str "loading " ++ str module_name ++ str "... "); try - (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in + (let qid = Libnames.qualid_of_ident (Names.id_of_string module_name) in require_library [dummy_loc,qid] None; msg (str "opening... "); Declaremods.import_module false (Nametab.locate_module qid); diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml index 668a581e1d..f5e8be31e0 100644 --- a/plugins/interface/name_to_ast.ml +++ b/plugins/interface/name_to_ast.ml @@ -106,7 +106,7 @@ let convert_one_inductive sp tyi = let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in let env = Global.env () in let envpar = push_rel_context params env in - let sp = sp_of_global (IndRef (sp, tyi)) in + let sp = path_of_global (IndRef (sp, tyi)) in (((false,(dummy_loc,basename sp)), convert_env(List.rev params), Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw , @@ -192,18 +192,6 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) = let name_to_ast ref = let (loc,qid) = qualid_of_reference ref in let l = - try - let sp = Nametab.locate_obj qid in - let (sp,lobj) = - let (sp,entry) = - List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None) - in - match entry with - | Lib.Leaf obj -> (sp,obj) - | _ -> raise Not_found - in - leaf_entry_to_ast_list (sp,lobj) - with Not_found -> try match Nametab.locate qid with | ConstRef sp -> constant_to_ast_list sp @@ -220,7 +208,7 @@ let name_to_ast ref = | Some c1 -> make_definition_ast name c1 typ []) with Not_found -> try - let _sp = Nametab.locate_syntactic_definition qid in + let _sp = Nametab.locate_syndef qid in errorlabstrm "print" (str "printing of syntax definitions not implemented") with Not_found -> diff --git a/plugins/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli index f9e83b5e1e..a532604f59 100644 --- a/plugins/interface/name_to_ast.mli +++ b/plugins/interface/name_to_ast.mli @@ -2,4 +2,4 @@ val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;; val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;; val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;; val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;; -val leaf_entry_to_ast_list : (Libnames.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;; +val leaf_entry_to_ast_list : (Libnames.full_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;; |