diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 2 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index b825262005..a4dc0eacd3 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -408,7 +408,7 @@ let inspect n = oname, Lib.Leaf lobj -> (match oname, object_tag lobj with (sp,_), "VARIABLE" -> - let (_, _, v) = get_variable (basename sp) in + let (_, _, v) = Global.lookup_named (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 172c7479c2..6b17e7396a 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -158,7 +158,7 @@ let constant_to_ast_list kn = 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 + let (id, c, v) = Global.lookup_named sp in let l = implicits_of_global (VarRef sp) in (match c with None -> |