diff options
| author | Pierre-Marie Pédrot | 2020-09-22 10:44:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:19:02 +0200 |
| commit | 2b91a8989687e152f7120aa6c907ffeba8495bab (patch) | |
| tree | 0fd0362eccc5c894b08c65147f0229fcdc8d2814 /pretyping/evarconv.ml | |
| parent | 8f16b1c5b97411b7ea88279699f0f410f1c77723 (diff) | |
Deprecate the non-qualified equality functions on kerpairs.
This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a5311e162d..6a668e79e8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -566,7 +566,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with - | Const (c, u), Const (c', u') when Constant.equal c c' -> + | Const (c, u), Const (c', u') when QConstant.equal env c c' -> let u = EInstance.kind evd u and u' = EInstance.kind evd u' in check_strict evd u u' | Const _, Const _ -> UnifFailure (evd, NotSameHead) @@ -844,7 +844,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty ise_try evd [f1; f2] (* Catch the p.c ~= p c' cases *) - | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' -> + | Proj (p,c), Const (p',u) when QConstant.equal env (Projection.constant p) p' -> let res = try Some (destApp evd (Retyping.expand_projection env evd p c [])) with Retyping.RetypeError _ -> None @@ -855,7 +855,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty appr2 | None -> UnifFailure (evd,NotSameHead)) - | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') -> + | Const (p,u), Proj (p',c') when QConstant.equal env p (Projection.constant p') -> let res = try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) with Retyping.RetypeError _ -> None |