From 9a3d4e284a03942e8a2b1f9d87a0b349702eaaa9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 17:56:33 +0200
Subject: Add missing deprecations in Projection API.

---
 kernel/names.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index 2445d1f309..9a4ceef802 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -662,14 +662,18 @@ module Projection : sig
   val unfold : t -> t
 
   val equal : t -> t -> bool
+  [@@ocaml.deprecated "Use QProjection.equal"]
   val hash : t -> int
+  [@@ocaml.deprecated "Use QProjection.hash"]
   val hcons : t -> t
   (** Hashconsing of projections. *)
 
   val repr_equal : t -> t -> bool
+  [@@ocaml.deprecated "Use an explicit projection of Repr"]
   (** Ignoring the unfolding boolean. *)
 
   val compare : t -> t -> int
+  [@@ocaml.deprecated "Use QProjection.compare"]
 
   val map : (MutInd.t -> MutInd.t) -> t -> t
   val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
-- 
cgit v1.2.3