aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index f5cb72f4e..c9a8cf6e1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -572,8 +572,8 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Proj of projection * 'constr
[@@ocaml.deprecated "Alias for Constr.kind_of_term"]
-type values = Constr.values
-[@@ocaml.deprecated "Alias for Constr.values"]
+type values = Vmvalues.values
+[@@ocaml.deprecated "Alias for Vmvalues.values"]
val hash_constr : Constr.constr -> int
[@@ocaml.deprecated "Alias for Constr.hash"]