aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r--kernel/nativelambda.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 508112b35..aaa9f9b00 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -378,7 +378,7 @@ module Renv =
type constructor_info = tag * int * int (* nparam nrealargs *)
type t = {
- name_rel : name Vect.t;
+ name_rel : Name.t Vect.t;
construct_tbl : constructor_info ConstrTable.t;
}