Merge PR #8780: Cleanup comparing projections through their constants.

2 files changed, 5 insertions, 0 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 7cd749de1d..18560d5f8d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -872,6 +872,8 @@ struct
 
   let equal (c, b) (c', b') = Repr.equal c c' && b == b'
 
+  let repr_equal p p' = Repr.equal (repr p) (repr p')
+
   let hash (c, b) = (if b then 0 else 1) + Repr.hash c
 
   module SyntacticOrd = struct
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