diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index d394bd1288..a3f1c0b004 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -311,7 +311,7 @@ let matches_core env sigma allow_bound_rels || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> - if Projection.equal pr1 pr then + if Environ.QProjection.equal env pr1 pr then try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure else raise PatternMatchingFailure @@ -332,7 +332,7 @@ let matches_core env sigma allow_bound_rels sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) - | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> + | PProj (p1,c1), Proj (p2,c2) when Environ.QProjection.equal env p1 p2 -> sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 1940668519..90af143a2d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -831,7 +831,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in ise_try evd [f1; f2] - | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' -> + | Proj (p, c), Proj (p', c') when QProjection.Repr.equal env (Projection.repr p) (Projection.repr p') -> let f1 i = ise_and i [(fun i -> evar_conv_x flags env i CONV c c'); diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b5c83b75f9..b259945d9e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -59,7 +59,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PCoFix (i1,f1), PCoFix (i2,f2) -> Int.equal i1 i2 && rec_declaration_eq f1 f2 | PProj (p1, t1), PProj (p2, t2) -> - Projection.equal p1 p2 && constr_pattern_eq t1 t2 + Projection.CanOrd.equal p1 p2 && constr_pattern_eq t1 t2 | PInt i1, PInt i2 -> Uint63.equal i1 i2 | PFloat f1, PFloat f2 -> |