aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/name_to_ast.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/name_to_ast.ml')
-rw-r--r--contrib/interface/name_to_ast.ml2
1 files changed, 1 insertions, 1 deletions
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 ->