diff options
Diffstat (limited to 'plugins/interface')
| -rw-r--r-- | plugins/interface/centaur.ml4 | 2 | ||||
| -rw-r--r-- | plugins/interface/name_to_ast.ml | 5 | ||||
| -rw-r--r-- | plugins/interface/name_to_ast.mli | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4 index e7084fbb00..07f32b6d43 100644 --- a/plugins/interface/centaur.ml4 +++ b/plugins/interface/centaur.ml4 @@ -416,7 +416,7 @@ let inspect n = | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_path sp)) (Pretyping.Default.understand Evd.empty (Global.env()) - (RRef(dummy_loc, IndRef(kn,0)))) + (RRef(dummy_loc, IndRef((mind_of_kn kn),0)))) | _ -> failwith ("unexpected value 1 for "^ (string_of_id (basename (fst oname))))) | _ -> failwith "unexpected value") diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml index ef61a8202d..142116adea 100644 --- a/plugins/interface/name_to_ast.ml +++ b/plugins/interface/name_to_ast.ml @@ -176,10 +176,11 @@ let inductive_to_ast_list sp = let leaf_entry_to_ast_list ((sp,kn),lobj) = let tag = object_tag lobj in + let con = constant_of_kn kn in match tag with | "VARIABLE" -> variable_to_ast_list (basename sp) - | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn) - | "INDUCTIVE" -> inductive_to_ast_list kn + | "CONSTANT" -> constant_to_ast_list con + | "INDUCTIVE" -> inductive_to_ast_list (mind_of_kn kn) | s -> errorlabstrm "print" (str ("printing of unrecognized object " ^ diff --git a/plugins/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli index a532604f59..db2555550e 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.full_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;; +val leaf_entry_to_ast_list : (Libnames.full_path * Names.kernel_name) * Libobject.obj -> Vernacexpr.vernac_expr list;; |