diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 2 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 3cc5390639..ef3561a708 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -413,7 +413,7 @@ let inspect n = let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> - let {const_type=typ} = Global.lookup_constant kn in + let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index a08f2cd6fc..0add95076a 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -173,9 +173,9 @@ let constant_to_ast_list kn = let l = implicits_of_global (ConstRef kn) in (match c with None -> - make_variable_ast (id_of_label (label kn)) typ l + make_variable_ast (id_of_label (con_label kn)) typ l | Some c1 -> - make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l) + make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = let (id, c, v) = get_variable sp in @@ -198,7 +198,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) = let tag = object_tag lobj in match tag with | "VARIABLE" -> variable_to_ast_list (basename sp) - | "CONSTANT" -> constant_to_ast_list kn + | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn) | "INDUCTIVE" -> inductive_to_ast_list kn | s -> errorlabstrm |