8000 Fix wrong threading of cv_pb/pb in unification.ml by mattam82 · Pull Request #20652 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fix wrong threading of cv_pb/pb in unification.ml #20652

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Fix wrong threading of cv_pb/pb in unification.ml #20652

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions pretyping/unification.ml
8000 View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1152,7 +1152,7 @@ let rec unify_0_with_initial_metas (subst : subst0) conv_at_top env cv_pb flags
| Evar (evk,_ as ev), Evar (evk',_)
when is_evar_allowed flags evk
&& Evar.equal evk evk' ->
begin match constr_cmp cv_pb env sigma flags cM cN with
begin match constr_cmp pb env sigma flags cM cN with
| Some sigma ->
push_sigma sigma substn
| None ->
Expand Down Expand Up @@ -1194,7 +1194,7 @@ let rec unify_0_with_initial_metas (subst : subst0) conv_at_top env cv_pb flags
(* Fast path for projections. *)
| Proj (p1,_,c1), Proj (p2,_,c2) when Environ.QConstant.equal env
(Projection.constant p1) (Projection.constant p2) ->
(try unify_same_proj curenvnb cv_pb {opt with at_top = true}
(try unify_same_proj curenvnb pb {opt with at_top = true}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this one seems like it should be constant CONV btw

substn c1 c2
with ex when precatchable_exception ex ->
6E87 unify_not_same_head curenvnb pb opt substn ~nargs cM cN)
Expand Down Expand Up @@ -1393,7 +1393,7 @@ let rec unify_0_with_initial_metas (subst : subst0) conv_at_top env cv_pb flags
let sigma = substn.subst_sigma in
try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
match constr_cmp cv_pb env sigma flags ~nargs cM cN with
match constr_cmp pb env sigma flags ~nargs cM cN with
| Some sigma -> push_sigma sigma substn
| None ->
try reduce curenvnb pb opt substn cM cN
Expand Down
Loading
0