aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r--pretyping/classops.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8707078b5..b41d0efac 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -17,9 +17,9 @@ type cl_typ =
| CL_SORT
| CL_FUN
| CL_SECVAR of variable
- | CL_CONST of constant
+ | CL_CONST of Constant.t
| CL_IND of inductive
- | CL_PROJ of constant
+ | CL_PROJ of Constant.t
(** Equality over [cl_typ] *)
val cl_typ_eq : cl_typ -> cl_typ -> bool