From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Nov 2017 18:58:27 +0100
Subject: [api] Deprecate all legacy uses of Names in core.

This will allow to merge back `Names` with `API.Names`
---
 pretyping/classops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/classops.mli')

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8707078b58..b41d0efac5 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
-- 
cgit v1.2.3