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/evarconv.ml     | 3 +--
 pretyping/reductionops.ml | 3 +--
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f0ff1aa93b..6a75be352b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -711,8 +711,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	in
 	ise_try evd [f1; f2]
 
-	| Proj (p, c), Proj (p', c') 
-	  when Constant.equal (Projection.constant p) (Projection.constant p') ->
+        | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' ->
 	  let f1 i = 
 	    ise_and i 
 	    [(fun i -> evar_conv_x ts env i CONV c c');
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