diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
index 8a3cfff41..024b86147 100644
--- a/src/coq_elpi_arg_HOAS.ml
+++ b/src/coq_elpi_arg_HOAS.ml
@@ -307,7 +307,7 @@ let of_coq_record_definition id =
     name;
     parameters = binders;
     sort;
-    constructor = Some idbuild;
+    constructor = Some idbuild.v;
     fields = cfs;
     univpoly = univpoly_of ~poly ~cumulative
   }