diff options
| author | Pierre-Marie Pédrot | 2020-09-23 17:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:27:39 +0200 |
| commit | 9a3d4e284a03942e8a2b1f9d87a0b349702eaaa9 (patch) | |
| tree | 796075d0664347a8704fd53ca1a96a0d1a48abfd /pretyping/constr_matching.ml | |
| parent | 373376b734343d86aecc8d1f91a8c78eefa2b6cc (diff) | |
Add missing deprecations in Projection API.
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 4 |
1 files changed, 2 insertions, 2 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) -> |