diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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'); |