aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/xml/xmlcommand.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 41967dede..df059677b 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -474,7 +474,7 @@ let kind_of_global r =
match r with
| Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
let isrecord =
- try let _ = Recordops.find_structure kn in true
+ try let _ = Recordops.lookup_structure kn in true
with Not_found -> false in
kind_of_inductive isrecord (fst kn)
| Ln.VarRef id -> kind_of_variable id