From 0ade32f84b28d2190360ec79520788142755b5b7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Mar 2018 20:29:16 +0100
Subject: [api] Deprecate a couple of aliases that we missed.

---
 kernel/typeops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index bff40b017f..85b2cfffde 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -60,7 +60,7 @@ val judge_of_constant : env -> pconstant -> unsafe_judgment
 
 (** {6 type of an applied projection } *)
 
-val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
+val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
 
 (** {6 Type of application. } *)
 val judge_of_apply :
@@ -100,7 +100,7 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-val type_of_projection_constant : env -> Names.projection puniverses -> types
+val type_of_projection_constant : env -> Projection.t puniverses -> types
 
 val type_of_constant_in : env -> pconstant -> types
 
-- 
cgit v1.2.3