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.

---
 pretyping/reductionops.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5dbe95a471..367a48cb5e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -398,8 +398,7 @@ struct
       match x, y with
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
         Constant.equal c1 c2 && Univ.Instance.equal u1 u2
-      | Cst_proj p1, Cst_proj p2 ->
-        Constant.equal (Projection.constant p1) (Projection.constant p2)
+      | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
       | _, _ -> false
     in
     let rec equal_rec sk1 sk2 =
-- 
cgit v1.2.3