From 0a50cfa8da5437ecd0b628eafcf48b60c7fd7676 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 19 Oct 2018 15:31:59 +0200
Subject: Cleanup comparing projections through their constants.

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

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index 37930c12e2..98995752a2 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -608,6 +608,9 @@ module Projection : sig
   val hcons : t -> t
   (** Hashconsing of projections. *)
 
+  val repr_equal : t -> t -> bool
+  (** Ignoring the unfolding boolean. *)
+
   val compare : t -> t -> int
 
   val map : (MutInd.t -> MutInd.t) -> t -> t
-- 
cgit v1.2.3